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