let k, n be natural Number ; :: thesis: ( k <> 0 implies (k * n) div k = n )
A0: ( k is Nat & n is Nat ) by TARSKI:1;
assume A1: k <> 0 ; :: thesis: (k * n) div k = n
k * n = (k * n) + 0 ;
hence (k * n) div k = n by A0, A1, Def1; :: thesis: verum