proposition: Lemma fib4S n: fib n.+4 = 3*(fib n.+1) + (fib n).*2.
proof: Proof. by rewrite fib3S fibSS doubleD addnAC - mul2n -mulSnr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)