for a, b, c being Real holds
( a <= b iff a + c <= b + c ) by Lm5, Lm10;