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