proposition: Lemma DE2_solution c d: DE_eq2 c d <-> (c=0 /\ d = 1) \/ exists n, c = fib n.*2.+2 /\ d = fib n.*2.+1.
proof: Proof. split; last first. case; [ by move => [-> ->] | move => [n [-> ->]]]. by elim:n => // n /DE2_rec; rewrite - fib3S - fibSS !doubleS. elim: c d {-2} c (leqnn c). move => d c; rewrite leqn0 /DE_eq2 => /eqP ->. rewrite {1} /expn /= addn0 add0n -{1} [1]/(1^2). by move/eqP; rewrite eqn_sqr => /eqP ->; left. move => n Hrec d c. rewrite leq_eqVlt ltnS; case /orP => [ha hb | le]; [right | by apply:Hrec ]. have cp: 0 < c by rewrite (eqP ha). move /andP: (DE2_pos cp hb) => [la lb]. have hc:= (DE2_rec' cp hb). have he: c - d <= n by rewrite (eqP ha) -(prednK (DE2_lt0d hb)) subSS leq_subr. move: (subnK (ltnW lb)) (subnK la); set a := c -d; set b := d.*2 - c => xv yv. have ra: d = a + b. by apply/eqP; rewrite - (eqn_add2r d) addnn - xv addnAC yv addnC. have rb: c = a.*2 + b by rewrite - yv ra addnA addnn. case: (Hrec _ _ he hc). by move => [sa sb]; exists 0; rewrite ra rb /a/b sa sb. move => [m [sa sb]]; exists m.+1. by rewrite ra rb /a/b sa sb -fibSS -fib3S !doubleS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)