proposition: Lemma SCF_pos2 a L : all (fun z => 0 < z) L -> a <= SCF (a::L).
proof: Proof. rewrite /SCF - {1}(addr0 a) lerD2l. case lz: (L== nil) => h; first by rewrite (eqP lz). by rewrite Order.POrderTheory.ltW ? SCF_pos1 ? 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)