proposition: Lemma CF_exists (x: rat): exists a l, good_for_cf a l /\ x = SCF (a::l).
proof: Proof. move: (floorp1 x) => /=; set a := (floorq x)%:~R => /andP[eq1 eq2]. have ra: rat_in_Z a by apply: rat_in_Z_int. have: 0 <= x - a < 1 by rewrite subr_ge0 eq1 ltrBlDr addrC eq2. rewrite Order.POrderTheory.le_eqVlt eq_sym subr_eq0. case:eqP => xa /=. by move => _; exists a, [::]; rewrite /= addr0 /good_for_cf ra. move /CF'_exists => [l lp xv]; exists a, l. by rewrite /good_for_cf andbA ra lp - xv addrC addrNK. 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)