proposition: Lemma SCF_pos1 L : all (fun z => 0 < z) L -> L != nil -> 0 < SCF' L.
proof: Proof. elim: L => // a L H /= /andP [ha hb] _; apply: divr_gt0 => //. case lz: (L== nil); first by rewrite (eqP lz) addr0. by apply: addr_gt0 => //; apply: H => //; rewrite lz. 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)