let k, m be Nat; :: thesis: ( k <> 0 implies (m * k) div k = m )
assume k <> 0 ; :: thesis: (m * k) div k = m
then ( ( m * k = (k * m) + 0 & 0 < k ) or ( m = 0 & k = 0 ) ) ;
hence (m * k) div k = m by Def1; :: thesis: verum