let b, a be real number ; :: thesis: ( b <= a & a <= 0 implies abs a <= abs b )
assume that
A1: b <= a and
A2: a <= 0 ; :: thesis: abs a <= abs b

per cases ( a = 0 or a < 0 ) by A2;

suppose a = 0 ; :: thesis: abs a <= abs b

then abs a = 0 by ABSVALUE:7;
hence abs a <= abs b by COMPLEX1:132; :: thesis: verum

end;

suppose A3: a < 0 ; :: thesis: abs a <= abs b

then A4: abs a = - a by ABSVALUE:def 1;
abs b = - b by A1, A3, ABSVALUE:def 1;
hence abs a <= abs b by A1, A4, XREAL_1:26; :: thesis: verum

end;

end;