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