let n be Nat; :: thesis: for a being Integer st n <> 0 holds

ex an being Nat st an,a are_congruent_mod n

let a be Integer; :: thesis: ( n <> 0 implies ex an being Nat st an,a are_congruent_mod n )

assume A1: n <> 0 ; :: thesis: ex an being Nat st an,a are_congruent_mod n

reconsider an = a mod n as Element of NAT by INT_1:3, INT_1:57;

take an ; :: thesis: an,a are_congruent_mod n

thus an,a are_congruent_mod n by A1, Lm7; :: thesis: verum

ex an being Nat st an,a are_congruent_mod n

let a be Integer; :: thesis: ( n <> 0 implies ex an being Nat st an,a are_congruent_mod n )

assume A1: n <> 0 ; :: thesis: ex an being Nat st an,a are_congruent_mod n

reconsider an = a mod n as Element of NAT by INT_1:3, INT_1:57;

take an ; :: thesis: an,a are_congruent_mod n

thus an,a are_congruent_mod n by A1, Lm7; :: thesis: verum