proposition: Lemma fib_square_succ n: (fib n.+2)^2 = (fib n.+1)^2 + (fib n)*(fib n.+3).
proof: Proof. rewrite fibSS sqrnD mulnA mulnC -(mulnn (fib n)) -addnA -mulnDr. by rewrite fibSS fibSS addnAC addnn mul2n (addnC (fib n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)