proposition: Lemma SCF_cat L1 L2 : L1 != nil -> L2 != nil -> SCF (L1 ++ L2) = SCF(rcons L1 (SCF L2)).
proof: Proof. case: L1 => // a L1 _ h /=; congr(a + _). elim: {a}L1 => //; first by rewrite /=addr0; move:h; case: L2 => //. by move => a l /= ->. 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)