let a, b, c be Real; :: thesis: ( a < 0 & b <= c implies b < c - a )
assume that
A1: a < 0 and
A2: b <= c ; :: thesis: b < c - a
a + b < c by A1, A2, Th37;
hence b < c - a by Lm19; :: thesis: verum