let n, m be Nat; :: thesis: ( 0 < m implies n mod m = n - (m * (n div m)) )
reconsider z1 = m * (n div m), z2 = n mod m as Integer ;
assume m > 0 ; :: thesis: n mod m = n - (m * (n div m))
then n - z1 = (z1 + z2) - z1 by NAT_D:2;
hence n mod m = n - (m * (n div m)) ; :: thesis: verum