let a, b, c, d be Real; :: thesis: ( a + b <= c - d implies a + d <= c - b )
assume A1: a + b <= c - d ; :: thesis: a + d <= c - b

per cases ( a + b <= c - d or b + a <= c - d ) by A1;

suppose a + b <= c - d ; :: thesis: a + d <= c - b

then (a + b) + d <= c by Lm17;
then (a + d) + b <= c ;
hence a + d <= c - b by Lm16; :: thesis: verum

end;

suppose b + a <= c - d ; :: thesis: a + d <= c - b

then (a + b) + d <= c by Lm17;
then (a + d) + b <= c ;
hence a + d <= c - b by Lm16; :: thesis: verum

end;

end;