proposition: Lemma DE2_sol n: (fib n.*2.+2)^2 + 1 = (fib n.*2.+1)^2 + (fib n.*2.+2)*(fib n.*2.+1).
proof: Proof. by apply/DE2_solution; right; exists n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)