let a, c, b be real number ; :: thesis: ( a < 0 & c <= b implies c + a < b )
assume that
A1: a < 0 and
A2: c <= b ; :: thesis: c + a < b
a + c < 0 + b by A1, A2, Lm8;
hence c + a < b ; :: thesis: verum