let n be natural Number ; :: thesis: n mod n = 0

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

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

n = (n * 1) + 0 ;
hence n mod n = 0 by A1, Def2; :: thesis: verum

end;

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

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

end;

end;