proposition: Lemma DE_eq6_pos x y: 0 <= y -> DE_eq6 x y -> exists n, y = (fib n.*2 * fib n.*2.+1)%N /\ (x = (fib n.*2.+1 ^ 2)%N \/ x = -((fib n.*2 ^ 2)%N:int)).
proof: Proof. rewrite DE_eq6_alt => sa /eqP. set z := (x *+ 2 - (y + 1)) => sb. have eq1: y = `|y|%N by move: sa; case y. have eq2: z ^+2 = ((`|z|)^2)%N. by rewrite - abszX; move: (sqr_ge0 z); case: (z^+2). have: DE_eq3 `|y| `|z|. move: sb; rewrite eq2 eq1 /DE_eq3 - PoszD addnn mulnn mulnn addn1. by case => <-. move/DE_eq3_solution => [n [ha hb]]; exists n. rewrite eq1 ha; split => //. have eq3: z = `|z|%:Z \/ z = - (`|z|%:Z) . by case: (z) => a; [left |right ]. have: x *+ 2 = z + (y+1) by rewrite /z subrK. have h u: (u.*2)%:Z = (u%:Z) *+ 2 by rewrite -muln2 PoszM - mulr_natr. case: eq3 => ->; rewrite hb eq1 ha - PoszD fib_doubleS mulnC. rewrite - addnA (addnA (fib n.*2 ^ 2)%N) -(DE1_sol n). by move/eqP;rewrite addnn h eqrMn2r /= => /eqP; left. move => hw; right; apply/eqP;move: (DE1_sol n) hw. rewrite -[X in _ *+2 = X] opprK opprD opprK - addnA addn1 => ->. by move/eqP; rewrite addnAC addnn PoszD addrK h -mulNrn eqrMn2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)