let n be Nat; :: thesis: for a being Integer st n <> 0 holds
a mod n,a are_congruent_mod n
let a be Integer; :: thesis: ( n <> 0 implies a mod n,a are_congruent_mod n )
assume A1: n <> 0 ; :: thesis: a mod n,a are_congruent_mod n
(a mod n) mod n = a mod n by INT_3:13;
hence a mod n,a are_congruent_mod n by A1, INT_3:12; :: thesis: verum