let a be Nat; :: thesis:
let k be Integer; :: thesis:
assume A1: ( a <> 0 & a gcd k = 1 ) ; :: thesis:
then A2: a >= 1 by NAT_1:14;

per cases by A2, XXREAL_0:1;

suppose A4: a = 1 ; :: thesis:

take b = 1; :: thesis:
take e = 1; :: thesis:
thus ( b <> 0 & e <> 0 ) ; :: thesis:
thus ( b <= sqrt a & e <= sqrt a ) by A4, SQUARE_1:83; :: thesis:
thus ( a divides (k * b) + e or a divides (k * b) - e ) by A4, INT_2:16; :: thesis:

end;

suppose A5: a > 1 ; :: thesis:

then A6: sqrt a < a by Lm24;
set d = [\(sqrt a)/];
set d1 = [\(sqrt a)/] + 1;
A7: sqrt a > 0 by A1, SQUARE_1:93;
A8: ( [\(sqrt a)/] <= sqrt a & [\(sqrt a)/] > (sqrt a) - 1 ) by INT_1:def 4;
then A9: [\(sqrt a)/] < a by A6, XXREAL_0:2;
sqrt a > 1 by A5, SQUARE_1:83, SQUARE_1:95;
then A10: (sqrt a) - 1 > 0 by XREAL_1:52;
then reconsider d = [\(sqrt a)/] as Element of NAT by A8, INT_1:16;
A11: ( d + 1 >= 1 & 1 > 0 ) by Lm1;
reconsider d1 = [\(sqrt a)/] + 1 as Element of NAT by A11;
set e1 = d1 ^2 ;
d1 ^2 = d1 * d1 ;
then reconsider e1 = d1 ^2 as Element of NAT ;
sqrt a < d1 by A8, XREAL_1:21;
then (sqrt a) ^2 < e1 by A7, SQUARE_1:78;
then A13: a < e1 by SQUARE_1:def 4;
deffunc H₁( Nat) -> Element of REAL = 1 + (((k * (($1 - 1) div d1)) + (($1 - 1) mod d1)) mod a);
consider fs being FinSequence such that
A14: ( len fs = e1 & ( for b being Nat st b in dom fs holds
fs . b = H₁(b) ) ) from FINSEQ_1:sch 2();
A16: Seg e1 = dom fs by A14, FINSEQ_1:def 3;
A17: rng fs c= Seg a

proof

let v be set ; :: according to TARSKI:def 3 :: thesis:
assume v in rng fs ; :: thesis:
then consider b being Nat such that
A18: ( b in dom fs & fs . b = v ) by FINSEQ_2:11;
A19: v = 1 + (((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a) by A14, A18;
then reconsider v1 = v as Integer ;
B20: 0 <= ((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a by NEWTON:78;
then A20: 1 <= v1 by A19, Lm1;
reconsider v1 = v1 as Element of NAT by B20, A19, INT_1:16;
((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a < a by A1, NEWTON:79;
then v1 <= a by A19, Lm9;
hence v in Seg a by A20; :: thesis:

end;

A21: Seg a c= Seg e1 by A13, FINSEQ_1:7;
rng fs <> dom fs by A13, A16, A17, FINSEQ_1:7;
then not fs is one-to-one by A16, A17, A21, FINSEQ_4:74, XBOOLE_1:1;
then consider v1, v2 being set such that
A22: ( v1 in dom fs & v2 in dom fs & fs . v1 = fs . v2 & v1 <> v2 ) by FUNCT_1:def 8;
reconsider v1 = v1, v2 = v2 as Element of NAT by A22;
A23: ( 1 <= v1 & v1 <= e1 & 1 <= v2 & v2 <= e1 ) by A14, A22, FINSEQ_3:27;
set x1 = (v1 - 1) div d1;
set x2 = (v2 - 1) div d1;
set x = ((v1 - 1) div d1) - ((v2 - 1) div d1);
set y1 = (v1 - 1) mod d1;
set y2 = (v2 - 1) mod d1;
set y = ((v1 - 1) mod d1) - ((v2 - 1) mod d1);
A24: ( ((v1 - 1) div d1) - ((v2 - 1) div d1) <> 0 or ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <> 0 )

proof

assume ( not ((v1 - 1) div d1) - ((v2 - 1) div d1) <> 0 & not ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <> 0 ) ; :: thesis:
then v1 - 1 = (((v2 - 1) div d1) * d1) + ((v2 - 1) mod d1) by A11, NEWTON:80
.= v2 - 1 by A11, NEWTON:80 ;
hence contradiction by A22; :: thesis:

end;

A25: ( (v1 - 1) mod d1 < d1 & (v2 - 1) mod d1 < d1 ) by A8, A10, NEWTON:79;
A26: ( (v1 - 1) mod d1 >= 0 & (v2 - 1) mod d1 >= 0 ) by NEWTON:78;
A27: abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) <= d

proof

((v1 - 1) mod d1) - ((v2 - 1) mod d1) < d1 by A25, A26, Lm3;
then A28: ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <= d by Lm9;
((v2 - 1) mod d1) - ((v1 - 1) mod d1) < d1 by A25, A26, Lm3;
then ((v2 - 1) mod d1) - ((v1 - 1) mod d1) <= d by Lm9;
then - (((v2 - 1) mod d1) - ((v1 - 1) mod d1)) >= - d by XREAL_1:26;
hence abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) <= d by A28, ABSVALUE:12; :: thesis:

end;

then A29: abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) < a by A9, XXREAL_0:2;
A30: abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) <= d

proof

A31: ( (v1 - 1) div d1 = [\((v1 - 1) / d1)/] & (v2 - 1) div d1 = [\((v2 - 1) / d1)/] ) by INT_1:def 7;
then A32: ( (v1 - 1) div d1 <= (v1 - 1) / d1 & (v2 - 1) div d1 <= (v2 - 1) / d1 ) by INT_1:def 4;
( v1 - 1 <= e1 - 1 & v2 - 1 <= e1 - 1 ) by A23, XREAL_1:11;
then A33: ( (v1 - 1) / d1 <= (e1 - 1) / d1 & (v2 - 1) / d1 <= (e1 - 1) / d1 ) by XREAL_1:74;
A34: (e1 - 1) / d1 = d1 - (1 / d1) by A11, XCMPLX_1:128;
1 / d1 > 0 by A8, A10, XREAL_1:141;
then (e1 - 1) / d1 < d1 by A34, Lm1;
then ( (v1 - 1) / d1 < d1 & (v2 - 1) / d1 < d1 ) by A33, XXREAL_0:2;
then ( (v1 - 1) div d1 < d1 & (v2 - 1) div d1 < d1 ) by A32, XXREAL_0:2;
then A35: ( (v1 - 1) div d1 <= d & (v2 - 1) div d1 <= d ) by Lm9;
A36: [\0 /] = 0 by INT_1:47;
( v1 - 1 >= 0 & v2 - 1 >= 0 ) by A23, XREAL_1:50;
then ( (v1 - 1) div d1 >= 0 & (v2 - 1) div d1 >= 0 ) by A31, A36, PRE_FF:11;
then A37: ( ((v1 - 1) div d1) - ((v2 - 1) div d1) <= d & ((v2 - 1) div d1) - ((v1 - 1) div d1) <= d ) by A35, Lm2;
then - (((v2 - 1) div d1) - ((v1 - 1) div d1)) >= - d by XREAL_1:26;
hence abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) <= d by A37, ABSVALUE:12; :: thesis:

end;

then A38: abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) < a by A9, XXREAL_0:2;
( fs . v1 = 1 + (((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) mod a) & fs . v2 = 1 + (((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) mod a) ) by A14, A22;
then A39: (((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1))) mod a = 0 by A22, Lm22, XCMPLX_1:2;
then A40: a divides ((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) by A1, Lm23;
A41: ((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) = (k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) ;
set d2 = (k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1));
A42: - ((k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) = (k * (- (((v1 - 1) div d1) - ((v2 - 1) div d1)))) + (- (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) ;

A43: now

assume A44: ((v1 - 1) div d1) - ((v2 - 1) div d1) = 0 ; :: thesis:
then a divides abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) by A40, Lm20;
then abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) = 0 by A29, NAT_D:7;
hence contradiction by A24, A44, ABSVALUE:7; :: thesis:

end;

A45: now

assume A46: ((v1 - 1) mod d1) - ((v2 - 1) mod d1) = 0 ; :: thesis:
then a divides ((v1 - 1) div d1) - ((v2 - 1) div d1) by A1, A39, A41, Lm23, Th36;
then a divides abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) by Lm20;
then abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) = 0 by A38, NAT_D:7;
hence contradiction by A24, A46, ABSVALUE:7; :: thesis:

end;

take b = abs (((v1 - 1) div d1) - ((v2 - 1) div d1)); :: thesis:
take e = abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)); :: thesis:
thus ( b <> 0 & e <> 0 ) by A43, A45, ABSVALUE:7; :: thesis:
thus b <= sqrt a by A8, A30, XXREAL_0:2; :: thesis:
thus e <= sqrt a by A8, A27, XXREAL_0:2; :: thesis:
( ( b = ((v1 - 1) div d1) - ((v2 - 1) div d1) or b = - (((v1 - 1) div d1) - ((v2 - 1) div d1)) ) & ( e = ((v1 - 1) mod d1) - ((v2 - 1) mod d1) or e = - (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) ) ) by ABSVALUE:1;
hence ( a divides (k * b) + e or a divides (k * b) - e ) by A40, A42, INT_2:14; :: thesis:

end;