proposition: Lemma SCF'_opp l: SCF' [seq -x | x <- l] = - SCF' l.
proof: Proof. case: l => // a l; elim: l a => [a | b l H a]. by rewrite /= !addr0 !div1r invrN. by move: (H b) => /= ->; rewrite - opprD !div1r invrN. 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)