let a, b be real number ; :: thesis: ( 0 <= a implies b <= a + b )
assume A1: 0 <= a ; :: thesis: b <= a + b
assume A2: a + b < b ; :: thesis: contradiction

per cases ( a + b < b or b - a > b ) by A2;

suppose a + b < b ; :: thesis: contradiction

then (a + b) - b < 0 by Lm23;
hence contradiction by A1; :: thesis: verum

end;

suppose b - a > b ; :: thesis: contradiction

then (b + (- a)) - b > 0 by Lm21;
hence contradiction by A1; :: thesis: verum

end;

end;