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

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

suppose A2: n = 0 ; :: thesis: m / n = m div n

hence m / n = 0
.= m div n by A2 ;
:: thesis: verum

end;

suppose A3: n <> 0 ; :: thesis: m / n = m div n

then i - ((i div n) * n) = 0 by A1, INT_1:def 10;
hence m / n = m div n by A3, XCMPLX_1:89; :: thesis: verum

end;

end;