proposition: Lemma DE_eq3_solution y z: DE_eq3 y z <-> (exists n, y = fib n.*2 * fib n.*2.+1 /\ z = fib (n.*2).*2.+1).
proof: Proof. split; last first. move => [n [-> ->]]; rewrite /DE_eq3 fib_doubleS. set a := fib n.*2.+1; set b := fib n.*2. have lea: b^2 <= a ^2 by rewrite leq_sqr fib_monotone. rewrite (sqrnD_sub' lea) -expnMn -[4]/(2^2) -expnMn mul2n mulnC addnC. rewrite eqn_add2r eqn_sqr -(eqn_add2r (b^2)) subnK // addnC. by rewrite -(addn1 (_ * _)) addnA mulnC - DE1_sol. case: (posnP y) => lt1 h. rewrite lt1; exists 0; split => //; rewrite fib1. by move: h; rewrite /DE_eq3 lt1 addn0 eqn_sqr => /eqP. set r := gcdn y.+1 y.*2. have: (y.+1)^2 + (y.*2)^2 = z^2 by rewrite (eqP h). case/pythagore_tripleB. + by move => []. + by move => []; move: lt1;case:(y). + move => [p [q [ha /ltnW hb hc hd]]]; case; case; rewrite -/r => e1 e2 e3. move /eqP: e2; rewrite -doubleMr eqn_double => /eqP e2. move: (dvdn_gcd r y y.+1); rewrite -{1} addn1 gcdnDl gcdn1 e1 e2. rewrite {2 3} /dvdn !modnMr eqxx /= dvdn1 => /eqP r1. move: e1 e2 e3; rewrite r1 !mul1n => e1 e2 e3. have l1: q^2 <= p^2 by rewrite leq_exp2r ? hb. move: (subnK l1); rewrite - e1 e2 addSn addnC - addn1; move/esym. move/(DE1_solution p q) => [n [ra rb]]; exists n. by rewrite e3 ra rb mulnC - fib_doubleS. + have : ~~ odd y.+1 by rewrite e2 - doubleMr odd_double. move => /= /negbNE oy. have g2: r = 2. rewrite /r -(odd_double_half y) oy add1n -doubleS -!muln2 - muln_gcdl. by rewrite (muln2 y./2) -addnn -addSn gcdnDl (eqP (coprimeSn y./2)). move: (pythagore_gcd hb hc hd). set p1 := p + q; set q1 := p - q. have pv: p.*2 = p1 + q1 by rewrite -addnn -{2} (subnKC hb) addnA. have qv: q.*2 = p1 - q1 by rewrite subnBA// - addnA addKn addnn. move/eqP: e1; rewrite g2 mul2n eqn_double subn_sqr => /eqP e1. move: e2; rewrite g2 doubleMr qv mulnA mul2n pv mulnC -subn_sqr e1 => e2. have: DE_eq1 p1 q1. by rewrite /DE_eq1 -addnA addn1 mulnC e2 subnKC // leq_exp2r // leq_BD. move/(DE1_solution) => [n [p1v p2v]]. have yv: y = fib n.*2 * fib n.*2.+1 by rewrite e1 -/p1 -/q1 p1v p2v. have : 2 * z = 2* fib (n.*2).*2.+1. rewrite e3 g2 mulnA mulnDr -[2*2]/(2^2) -!expnMn !mul2n pv qv p1v p2v -fibSS. by case:(n)=> // m; rewrite doubleS (fibSS m.*2.+1) addKn fib_square_n3_n. move/eqP; rewrite !mul2n eqn_double => /eqP zv. by exists n; rewrite - yv - e1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)