let n, k be Nat; :: thesis: ( k <> 0 implies n,n mod k are_congruent_mod k )
assume k <> 0 ; :: thesis: n,n mod k are_congruent_mod k
then (n mod k) - 0 = n - ((n div k) * k) by INT_1:def 10;
then k divides n - (n mod k) by INT_1:def 3;
hence n,n mod k are_congruent_mod k by INT_1:def 4; :: thesis: verum