let n, i, j be Nat; :: thesis: ( Fib n, Fib (n + i) are_congruent_mod j & Fib (n + 1), Fib ((n + i) + 1) are_congruent_mod j implies for x, y being Nat st x,y are_congruent_mod i holds
Fib x, Fib y are_congruent_mod j )
assume A1: ( Fib n, Fib (n + i) are_congruent_mod j & Fib (n + 1), Fib ((n + i) + 1) are_congruent_mod j ) ; :: thesis: for x, y being Nat st x,y are_congruent_mod i holds
Fib x, Fib y are_congruent_mod j
defpred S1[ Nat] means ( Fib $1, Fib ($1 + i) are_congruent_mod j & Fib ($1 + 1), Fib (($1 + i) + 1) are_congruent_mod j );
defpred S2[ Nat] means S1[n + $1];
A2: S2[ 0 ] by A1;
A3: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A4: S2[k] ; :: thesis: S2[k + 1]
(Fib (n + k)) + (Fib ((n + k) + 1)),(Fib ((n + k) + i)) + (Fib (((n + k) + i) + 1)) are_congruent_mod j by A4, INT_1:16;
then Fib (((n + k) + 1) + 1),(Fib ((n + k) + i)) + (Fib (((n + k) + i) + 1)) are_congruent_mod j by PRE_FF:1;
hence S2[k + 1] by A4, PRE_FF:1; :: thesis: verum
end;
A5: for k being Nat holds S2[k] from NAT_1:sch 2(A2, A3);
 defpred S3[ Nat] means ( $1 <= n implies for i being Nat st i = n - $1 holds
S1[i] );
A6: S3[ 0 ] by A1;
A7: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A8: ( S3[k] & k + 1 <= n ) ; :: thesis: for i being Nat st i = n - (k + 1) holds
S1[i]
let z be Nat; :: thesis: ( z = n - (k + 1) implies S1[z] )
assume A9: z = n - (k + 1) ; :: thesis: S1[z]
A10: ( (Fib z) + (Fib (z + 1)) = Fib ((z + 1) + 1) & (Fib (z + i)) + (Fib ((z + i) + 1)) = Fib (((z + 1) + i) + 1) ) by PRE_FF:1;
S1[z + 1] by A8, NAT_1:13, A9;
then (Fib ((z + 1) + 1)) - (Fib (z + 1)),(Fib (((z + 1) + i) + 1)) - (Fib ((z + 1) + i)) are_congruent_mod j by INT_1:17;
hence S1[z] by A10, A8, NAT_1:13, A9; :: thesis: verum
end;
A11: for k being Nat holds S3[k] from NAT_1:sch 2(A6, A7);
 A12: for k being Nat holds Fib k, Fib (k + i) are_congruent_mod j
proof
let k be Nat; :: thesis: Fib k, Fib (k + i) are_congruent_mod j
per cases ( k < n or k >= n ) ;
suppose k < n ; :: thesis: Fib k, Fib (k + i) are_congruent_mod j
then reconsider z = n - k as Element of NAT by NAT_1:21;
A13: S3[z] by A11;
z <= n - 0 by XREAL_1:10;
hence Fib k, Fib (k + i) are_congruent_mod j by A13; :: thesis: verum
end;
suppose k >= n ; :: thesis: Fib k, Fib (k + i) are_congruent_mod j
then reconsider z = k - n as Element of NAT by NAT_1:21;
S2[z] by A5;
hence Fib k, Fib (k + i) are_congruent_mod j ; :: thesis: verum
end;
end;
end;
A14: now :: thesis: for x, y being Nat st x < y & x,y are_congruent_mod i holds
Fib x, Fib y are_congruent_mod j
let x, y be Nat; :: thesis: ( x < y & x,y are_congruent_mod i implies Fib x, Fib y are_congruent_mod j )
assume A15: ( x < y & x,y are_congruent_mod i ) ; :: thesis: Fib x, Fib y are_congruent_mod j
consider k being Integer such that
A16: y = (k * i) + x by NAT_6:9, A15, INT_1:14;
y >= x + 0 by A15;
then k >= 0 by A15, A16, XREAL_1:7;
then reconsider k = k as Element of NAT by INT_1:3;
defpred S4[ Nat] means Fib x, Fib (x + (i * $1)) are_congruent_mod j;
A17: S4[ 0 ] by INT_1:11;
A18: for k being Nat st S4[k] holds
S4[k + 1]
proof
let k be Nat; :: thesis: ( S4[k] implies S4[k + 1] )
assume A19: Fib x, Fib (x + (i * k)) are_congruent_mod j ; :: thesis: S4[k + 1]
Fib (x + (i * k)), Fib ((x + (i * k)) + i) are_congruent_mod j by A12;
hence S4[k + 1] by A19, INT_1:15; :: thesis: verum
end;
for k being Nat holds S4[k] from NAT_1:sch 2(A17, A18);
then S4[k] ;
hence Fib x, Fib y are_congruent_mod j by A16; :: thesis: verum
end;
let x, y be Nat; :: thesis: ( x,y are_congruent_mod i implies Fib x, Fib y are_congruent_mod j )
assume A20: x,y are_congruent_mod i ; :: thesis: Fib x, Fib y are_congruent_mod j
A21: y,x are_congruent_mod i by A20, INT_1:14;
per cases ( x < y or x = y or y < x ) by XXREAL_0:1;
suppose x < y ; :: thesis: Fib x, Fib y are_congruent_mod j
hence Fib x, Fib y are_congruent_mod j by A20, A14; :: thesis: verum
end;
suppose x = y ; :: thesis: Fib x, Fib y are_congruent_mod j
hence Fib x, Fib y are_congruent_mod j by INT_1:11; :: thesis: verum
end;
suppose y < x ; :: thesis: Fib x, Fib y are_congruent_mod j
then Fib y, Fib x are_congruent_mod j by A14, A21;
hence Fib x, Fib y are_congruent_mod j by INT_1:14; :: thesis: verum
end;
end;