proposition: Lemma CF_bound a l: good_for_cf a l -> floorq a = floorq (SCF (a::l)).
proof: Proof. move => /and3P [ha hb hc]. have ap:= (all_rat_in_P_pos hb). apply: floorp2;rewrite -(eqP ha)(SCF_pos2 _ ap) /= ltrD2l. move: hb hc ap; case:l => // c l hb hc /= /andP[_ ap]. suff ww: 1 < c + SCF' l by rewrite /= div1r invf_lt1 // (Order.POrderTheory.lt_trans ltr01 ww). move: hb => /= /andP [/rat_in_P_ge1 cp hb]. case lz: (l== [::]). move:hc lz cp; clear;case: l => //= ca _ cb. by rewrite addr0 Order.POrderTheory.lt_neqAle eq_sym ca cb. have la: 0 < SCF' l by apply:SCF_pos1 =>//; rewrite lz. by move:(ler_ltD cp la); rewrite addr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)