let x be real number ; :: thesis: ( 0 <= x & x <= 1 implies x ^2 <= x )
assume A1: ( 0 <= x & 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 A2: 0 < x ; :: thesis: x ^2 <= x

per cases ( x = 1 or x < 1 ) by A1, 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 A2, Th75; :: thesis: verum

end;

end;

end;

end;