proposition: Lemma SCF_recl L a b: SCF (rcons (rcons L a) b) = SCF (rcons L (a+1/b)).
proof: Proof. case: L; first by rewrite /SCF /= !addr0. by move => u v;rewrite - cats1 cat_rcons SCF_cat // SCF2. 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)