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

now

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