proposition: Lemma DE_eq6_neg x y: y <0 -> DE_eq6 x y -> exists n, y = -((fib n.*2.+2 * fib n.*2.+1)%N:int) /\ (x = (fib n.*2.+1 ^ 2)%N \/ x = -((fib n.*2.+2 ^ 2)%N:int)).
proof: Proof. rewrite DE_eq6_alt => sa /eqP. set z := (x *+ 2 - (y + 1)) => eq0. have eq2: z ^+2 = ((`|z|)^2)%N. by rewrite - abszX; move: (sqr_ge0 z); case: (z^+2). have eq1: -y = `|y|%N by move: sa; case y. have eq3 : (`|y|%:Z - 1) = (`|y|.-1)%N. by move: sa; clear;case: y => //; case. have yp : 0 < `|y| by move: sa; case y. have: DE_eq4 `|y| `|z|. move: eq0; rewrite eq2 - sqrrN - (sqrrN (y *+ 2)) opprD -mulNrn. by rewrite eq1 eq3 - PoszD addnn mulnn mulnn; case => /eqP. move/(DE_eq4_solution _ yp) => [n [ha hb]]; exists n; split. by apply: oppr_inj; rewrite opprK eq1 ha. have eq4: z = `|z|%:Z \/ z = - (`|z|%:Z) by case: (z) => a; [left |right ]. have h u: (u.*2)%:Z = (u%:Z) *+ 2 by rewrite -muln2 PoszM - mulr_natr. have: x *+ 2 = z +1 + (-(-y)) by rewrite opprK addrAC -addrA /z subrK. case: eq4 => ->; rewrite hb -doubleS fib_doubleS eq1 ha. rewrite - (PoszD _ 1%N) addnAC (DE2_sol n) addnAC PoszD addrK addnn. by move/eqP; rewrite h eqrMn2r /= => /eqP; left. move => hw; right; apply/eqP; move /eqP: hw. rewrite addrAC -opprD - PoszD - addnA -(DE2_sol n) addnA addnn PoszD opprD. by rewrite 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)