let n, m be Nat; :: thesis: ( m / n = m div n implies m mod n = 0 )
assume A1: m / n = m div n ; :: thesis: m mod n = 0

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

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

hence m mod n = 0 ; :: thesis: verum

end;

suppose A2: n > 0 ; :: thesis: m mod n = 0

then m + 0 = (n * (m / n)) + (m mod n) by A1, NAT_D:2;
then (m mod n) - 0 = m - (n * (m / n)) ;
hence m mod n = m - m by A2, XCMPLX_1:87
.= 0 ;
:: thesis: verum

end;

end;