let a, b, c, d be Real; :: thesis: ( a < b & c <= d implies a + c < b + d )
assume that
A1: a < b and
A2: c <= d ; :: thesis: a + c < b + d
for a, b, c, d being Real st a < b & c <= d holds
a + c < b + d
proof
let a, b, c, d be Real; :: thesis: ( a < b & c <= d implies a + c < b + d )
assume A3: a < b ; :: thesis: ( not c <= d or a + c < b + d )
assume A4: c <= d ; :: thesis: a + c < b + d
A5: a + c <> b + d
proof
a + c <= d + a by A4, Lm5;
then A6: (a + c) - d <= (a + d) - d by Lm7;
assume a + c = b + d ; :: thesis: contradiction
hence contradiction by A3, A6; :: thesis: verum
end;
a + c <= b + d by A3, A4, Lm6;
hence a + c < b + d by A5, XXREAL_0:1; :: thesis: verum
end;
hence a + c < b + d by A1, A2; :: thesis: verum