let a, b, c be Real; :: 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