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