proposition: Lemma frac_continuant a l: all (fun z => 0 < z) l -> SCF (a :: l) = K (a::l) / K l.
proof: Proof. elim: l a => [a | b l H a apl];first by rewrite /= addr0 divr1. move: (continuant_gt0 apl); rewrite lt0r => /andP [kp _]. move/andP: apl => [_ apl]. by rewrite continuantS mulrDl mulrK // SCF_rec H // div1r invf_div. 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)