let n be Nat; :: thesis: n mod n = 0

per cases ( n > 0 or n = 0 ) ;

suppose A1: n > 0 ; :: thesis: n mod n = 0

ex p being Nat st
( n = (n * p) + 0 & 0 < n )

proof

n = (n * 1) + 0 ;
hence ex p being Nat st
( n = (n * p) + 0 & 0 < n ) by A1; :: thesis: verum

end;

hence n mod n = 0 by Def2; :: thesis: verum

end;

suppose n = 0 ; :: thesis: n mod n = 0

hence n mod n = 0 by Def2; :: thesis: verum

end;

end;