let a be real number ; :: thesis: 0 <= a * a

per cases ( 0 <= a or not 0 <= a ) ;

suppose 0 <= a ; :: thesis: 0 <= a * a

then 0 * a <= a * a ;
hence 0 <= a * a ; :: thesis: verum

end;

suppose not 0 <= a ; :: thesis: 0 <= a * a

then 0 * a <= a * a ;
hence 0 <= a * a ; :: thesis: verum

end;

end;