proposition: Lemma FR_fib_sum9 i: FR ((fib i.+4) * 2) = ((i./2)*2).+2.
proof: Proof. by rewrite fib_times2 (_: i.+1.+4 = 1 + 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)