proposition: Lemma DE1_solution c d: DE_eq1 c d <-> exists n, c = fib n.*2.+1 /\ d = fib n.*2.
proof: Proof. split; last first. move => [n [-> ->]];apply /DE_equiv_12; rewrite - fibSS. by apply/DE2_solution; right; exists n. case/DE_equiv_12/DE2_solution => [[/eqP] | [n [sa sb]]]. by rewrite addn_eq0 => /andP[/eqP ->]. by exists n; move/eqP: sa; rewrite fibSS - sb eqn_add2l => /eqP ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)