let k, n be Nat; :: thesis: ( k <> 0 implies (n + k) div k = (n div k) + 1 )
assume k <> 0 ; :: thesis: (n + k) div k = (n div k) + 1
then consider t being Nat such that
A1: n = (k * (n div k)) + t and
A2: t < k by NAT_D:def 1;
n + k = (k * ((n div k) + 1)) + t by A1;
hence (n + k) div k = (n div k) + 1 by A2, NAT_D:def 1; :: thesis: verum