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