let x be Real; :: thesis: ( 0 <= x & x <= 1 implies x ^2 <= x )
assume that
A1: 0 <= x and
A2: x <= 1 ; :: thesis: x ^2 <= x

per cases ( 0 = x or 0 < x ) by A1;

suppose 0 = x ; :: thesis: x ^2 <= x

hence x ^2 <= x ; :: thesis: verum

end;

suppose A3: 0 < x ; :: thesis: x ^2 <= x

per cases ( x = 1 or x < 1 ) by A2, XXREAL_0:1;

suppose x = 1 ; :: thesis: x ^2 <= x

hence x ^2 <= x ; :: thesis: verum

end;

suppose x < 1 ; :: thesis: x ^2 <= x

hence x ^2 <= x by A3, Th13; :: thesis: verum

end;

end;

end;

end;