proposition: Lemma fib_times4 i: (fib i.+2) * 4 = fib i.+4 + fib i.+2 + fib i.
proof: Proof. rewrite (fibSS i.+2) - addnA - addnA (addnA (fib i.+2)) addnn. by rewrite (fibSS i.+1) addnACA - fibSS - muln2 - mulnS - mulnSr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)