let n, m be Nat; :: thesis: ( n > 1 & m > 1 & m,1 are_congruent_mod n implies m mod n = 1 )
assume A1: ( n > 1 & m > 1 & m,1 are_congruent_mod n ) ; :: thesis: m mod n = 1
then consider d being Integer such that
A2: n * d = m - 1 by INT_1:def 3;
m - 1 > 1 - 1 by A1, XREAL_1:11;
then d > 0 by A2;
then reconsider d = d as Element of NAT by INT_1:16;
m = (n * d) + 1 by A2;
then m mod n = 1 mod n by NAT_D:21
.= 1 by A1, NAT_D:14 ;
hence m mod n = 1 ; :: thesis: verum