let m, n be Nat; :: thesis: ( n > 1 implies ( m mod n = 1 iff m,1 are_congruent_mod n ) )
assume A1: n > 1 ; :: thesis: ( m mod n = 1 iff m,1 are_congruent_mod n )
A2: ( m,1 are_congruent_mod n implies m mod n = 1 )

proof

assume m,1 are_congruent_mod n ; :: thesis: m mod n = 1
then consider t being Integer such that
A3: n * t = m - 1 ;
reconsider m = m, n = n as Integer ;
m mod n = ((n * t) + 1) mod n by A3
.= 1 mod n by NAT_D:61 ;
hence m mod n = 1 by A1, NAT_D:14; :: thesis: verum

end;

( m mod n = 1 implies m,1 are_congruent_mod n )

proof

assume m mod n = 1 ; :: thesis: m,1 are_congruent_mod n
then consider k being Nat such that
A4: m = (n * k) + 1 and
1 < n by NAT_D:def 2;
n * k = m - 1 by A4;
hence m,1 are_congruent_mod n ; :: thesis: verum

end;

hence ( m mod n = 1 iff m,1 are_congruent_mod n ) by A2; :: thesis: verum