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