proposition: Lemma DE_eq4_solution y z: 0 < y -> (DE_eq4 y z <-> exists n, y = fib n.*2.+2 * fib n.*2.+1 /\ z = fib (n.*2).*2.+3).
proof: Proof. move => yp; split; last first. move => [n [-> ->]]; rewrite /DE_eq4 - doubleS fib_doubleS. set a := fib n.*2.+2 ; set b := fib n.*2.+1. have lea: b^2 <= a ^2 by rewrite leq_sqr fib_monotone. have /prednK ww : 0 < a * b by rewrite muln_gt0 !fib_gt0. rewrite (sqrnD_sub' lea) -expnMn -[4]/(2^2) -expnMn mul2n mulnC addnC. rewrite eqn_add2r eqn_sqr -(eqn_add2r (b^2)) subnK // addnC mulnC. by rewrite - eqSS - addnS ww - (DE2_sol n) addn1. have yn := (prednK yp). move => h. have h': (y.-1)^2 + (y.*2)^2 = z^2 by rewrite (eqP h). case:(pythagore_tripleB h'). + by move => [/eqP]; rewrite - eqSS yn =>/eqP -> <-; exists 0. + by move => []; move: yp; case: (y) => //. + move=> [p [q [ha /ltnW hb hc hd]]]. case; case; set r := gcdn y.-1 y.*2 => e1 e2 e3. move /eqP: e2; rewrite -doubleMr eqn_double => /eqP e2. move: (dvdn_gcd r y y.-1); rewrite -{1} yn gcdnC -{1} addn1 gcdnDl. rewrite gcdn1 e1 e2 {2 3} /dvdn !modnMr eqxx /= dvdn1 => /eqP r1. move: e1 e2 e3; rewrite r1 !mul1n => e1 e2 e3. have /DE2_solution: (DE_eq2 p q). rewrite /DE_eq2 - e2 -yn e1 [in RHS] addnS. by rewrite addn1 subnKC // leq_exp2r ? hb. case; first by move => [pz]; move: yp; rewrite e2 pz. by move => [n [he hf]]; exists n; rewrite e3 he hf - fib_doubleS. + have oy: odd y.-1 = false. by move: (f_equal odd e2); rewrite -doubleMr odd_double. have g2: r = 2. rewrite /r -{2} yn - (odd_double_half y.-1) oy add0n. rewrite -!muln2 - muln_gcdl (muln2 y.-1./2) -addnn - addSn. by rewrite gcdnDr gcdnC (eqP (coprimeSn y.-1./2)). 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/eqP: e2; rewrite - eqSS yn g2 doubleMr qv mulnA mul2n pv mulnC. rewrite -subn_sqr e1 -/p1 -/q1 mulnC => /eqP e2. have: DE_eq2 p1 q1. by rewrite /DE_eq2 e2 -(addn1 (_ - _)) addnA subnKC // leq_exp2r // leq_BD. case/(DE2_solution). by move => [/eqP]; rewrite /p1 /q1 addn_eq0 => /andP[/eqP -> /eqP ->]. move=> [n [p1v p2v]]; exists n; rewrite p1v p2v; split => //. apply/eqP; rewrite - eqn_double -!mul2n e3 g2 mulnA -[2 *2]/(2^2). rewrite mulnDr -!expnMn ! mul2n pv qv p1v p2v - fibSS (fibSS n.*2) addKn. by rewrite fib_square_n3_n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)