proposition: Lemma CF'_exists (x: rat): 0<x<1 -> exists2 l, (all rat_in_P l && (last 0 l !=1)) & x = SCF' l.
proof: Proof. move => /andP [xp xl1]. have nqp: (0 < numq x) by rewrite (numq_gt0 x) xp. have: `|numq x|%N = numq x :> int by rewrite abszE; move: nqp;case: (numq x). move: (absz_denq x); set b := absz _; set a := absz _ => bv av. have bp: (0 < b)%N by move: (denq_gt0 x); rewrite - bv; case: (b). move: (divq_num_den x); rewrite - bv - av => xv. case: (posnP a) => ap; first by move: xp; rewrite - xv ap mul0r. have: x * b%:~R < b%:~R by rewrite gtr_pMl // ltr0n. rewrite bv - (numqE x) - bv - av ltr_int ltz_nat - xv => lab. move: ap lab; move: (leqnn b); clear; move:a b {-2} (b) => a n b {x}. elim: n a b. by move => a b h1 h2 h3; move: (leq_trans h3 h1); rewrite ltn0. move => n Hrec a b lbn ap lab. have dvde:=(divn_eq b a). have R3:=(ltn_pmod b ap). case: (posnP (b %/ a)) => qp. by move: dvde (ltnW lab);rewrite qp mul0n add0n leqNgt=> ->; rewrite R3. set q := (b %/ a)%:Z%:Q. have ap':a%:Z%:Q != 0 by rewrite intq_eq0; move: ap; case (a). have ->: a%:~R / b%:~R = 1 / (q + (b %% a)%R%:~R / a%:~R). by rewrite - invf_div div1r {1}dvde ratN_D mulrDl ratN_M mulfK. have rq: rat_in_P q. by rewrite /q -{1} (prednK qp) rat_in_P_nat /=. case: (posnP (b %% a)) => R2. move: dvde; rewrite R2 addn0 mul0r => bv. exists [:: q] => //=; rewrite rq /= pnatr_eq1;case q1: (b %/ a == 1%N) => //. by move: lab; rewrite bv (eqP q1) mul1n ltnn. have R1: (a <= n)%N by move: (leq_trans lab lbn); rewrite ltnS. move: (Hrec _ _ R1 R2 R3) => [l /andP[ha hb] hc]. exists (q :: l); rewrite ? hc //= ha rq /=. move: hb hc;case: (l) => //= _ /eqP. by rewrite mulf_eq0 invr_eq0 (negbTE ap') orbF intq_eq0; move: R2; case:(b%%a). 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)