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