proposition: Lemma fib_times2 i: (fib i.+2) * 2 = fib i.+3 + fib i.
proof: Proof. by rewrite muln2 - addnn {1} fibSS addnAC (addnC (fib i.+1)) - fibSS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)