proposition: Lemma FR_fib_sum1 i k: 2 <= k -> FR(fib (i+ k.+2) + fib k) = (i.+3)./2 + (k./2).-1 * (i.+4)./2.
proof: Proof. move => kp. have eq1: k = k.-2.+2 by move: kp; case:k => // [] []. set l := [:: k+i ; k.-2]. have sl: sorted ggen l by rewrite /= - eq1 leq_addr. move: (ZeckP sl); rewrite {1}/l /Zeck_val !big_cons big_nil - eq1 addn0. rewrite (addnC k) - ! addnS; set n:= (fib (i+ k.+2) + fib k) => eq2. rewrite FR_prop8 /Zeck_li eq2 /l /= - eq1 /n addnK. have ->: (Zeckpn k.-2 (fib (i + k.+2))) = fib (i + 4). rewrite {2} eq1 -!addSnnS addn0 addnC; elim: (k.-2) (i.+3) => // h H /= j. by rewrite addSnnS H Zeckp_fib. by rewrite addn4 Zeckp_fib !FR_fib {2} eq1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)