proposition: Lemma FR_fib_sum10 i: FR ((fib i.+4) * 3) = ((i./2)*3).+2.
proof: Proof. by rewrite fib_times3 (_: i.+2.+4 = 2 + i.+4) // FR_fib_sum1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)