let n be Nat; :: thesis: 0 div n = 0
now :: thesis: 0 div n = 0
per cases ( ex t being Nat st
( 0 = (n * (0 div n)) + t & t < n ) or ( 0 div n = 0 & n = 0 ) ) by NAT_D:def 1;
suppose A1: ex t being Nat st
( 0 = (n * (0 div n)) + t & t < n ) ; :: thesis: 0 div n = 0
then n * (0 div n) = 0 ;
hence 0 div n = 0 by A1, XCMPLX_1:6; :: thesis: verum
end;
suppose ( 0 div n = 0 & n = 0 ) ; :: thesis: 0 div n = 0
hence 0 div n = 0 ; :: thesis: verum
end;
end;
end;
hence 0 div n = 0 ; :: thesis: verum