proposition: Lemma fib_square_n3_n n: fib n.+3 ^ 2 + fib n ^ 2 = (fib (n.*2.+3)).*2.
proof: Proof. apply/eqP. rewrite -(eqn_add2l (fib (n.+1).*2.+1)) {1} fib_doubleS addnAC addnA. rewrite (addnC (fib n.+2 ^ 2)) -fib_doubleS -addnA (addnC (fib n ^2)). by rewrite - fib_doubleS !doubleS fib3S - addnA - fibSS addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)