proposition: Lemma FR_fib_sum2 i j k : 2 <= k -> k.+2 <= j -> j.+2 <= i -> FR(fib i + fib j + fib k) = (i-j+1)./2 + ((j-k-1)./2) * (i-j+2)./2 + (k./2.-1)*( (i-j+1)./2 + (j-k)./2 * (i-j+2)./2).
proof: Proof. move => ha hb hc. have eq1: k = k.-2.+2 by move: ha; case k => // [] []. have eq2: j = j.-2.+2 by move: hb; case j => // [] []. have eq3: i = i.-2.+2 by move: hc; case i => // [] []. set l := [:: i.-2; j.-2 ; k.-2]. have sl: sorted ggen l. rewrite /= - eq1 - eq2 - (ltnS j) - (ltnS j.+1) - eq3 hc. by rewrite - (ltnS k) - (ltnS k.+1) - eq2 hb. move: (ZeckP sl); rewrite {1}/l /Zeck_val !big_cons big_nil -eq1 -eq2 -eq3. rewrite addn0 addnA; set n := (fib i + fib j + fib k) => eq4. have eq5: (n - fib k) = fib i + fib j by rewrite /n addnK. rewrite FR_prop8 /Zeck_li eq4 /l /= - eq1 eq5 {5} eq1. rewrite -(subnK hc); set i1 := i - j.+2. rewrite -(subnK hb); set j1 := j - k.+2. rewrite - addSnnS - addSnnS - addSnnS - addSnnS !addnK !addn1 addnA. pose A n := (fib (i1.+2 + j1.+2 + n) + fib (j1.+2 + n)). have Av m: A m = (fib (i1 + (j1.+2 + m).+2) + fib (j1.+2 + m)). by rewrite /A - addnA addSnnS addSnnS. have zl m: Zeck_val [:: (i1.+2 + j1 + m); (j1 + m) ] = A m. by rewrite /Zeck_val !big_cons big_nil addn0 /A !addnS ! addSn. have zl' m: Zeck_valp [:: (i1.+2 + j1 + m.+1); (j1 + m.+1) ] = A m. by rewrite /Zeck_valp !big_cons big_nil addn0 /A !addnS ! addSn. have aux: forall n, Zeckp (A n.+1) = A n. move => m. rewrite - zl Zeckp_prop1 // /= mem_seq1 andbT -addnA. by rewrite - {2} (add0n (j1 + m.+1)) eqn_add2r. have aux2 a b: (Zeckpn a (A (a+b))) = A b. by elim: a b => // a H b /=; rewrite addSnnS H aux. rewrite -/(A _) {2 5} eq1 - addn2 aux2 aux Av Av addn1 FR_fib_sum1 // !addn2. rewrite FR_fib_sum1 // subn1 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)