proposition: Lemma FR_fib_sum4 i j : 5 <= j -> j.+2 <= i -> FR(fib i + fib j + 2) = (i-j+1)./2 + (j-4)./2 * (i-j+2)./2.
proof: Proof. move => ha hb; have hc:=(subnK (ltn_trans (leqnn 4) ha)). by rewrite (FR_fib_sum2 (leqnSn 2) ha hb) mul0n -subnDA addn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)