let m, n be Nat; :: thesis: ( m <> 0 & m divides n mod m implies m divides n )
assume A1: ( m <> 0 & m divides n mod m ) ; :: thesis: m divides n
then consider x being Nat such that
A2: n mod m = m * x by NAT_D:def 3;
A3: m > 0 by A1;
(n mod m) + (m * (n div m)) = m * (x + (n div m)) by A2;
then n = m * (x + (n div m)) by A3, NAT_D:2;
hence m divides n by NAT_D:def 3; :: thesis: verum