proposition: Lemma SCF_neg1 a b l l' (x := SCF' l') : b - 1 - x != 0 -> b - x != 0 -> SCF(l++a::-b::l') = SCF(l++a-1::1::b-1:: [seq -x | x <- l']).
proof: Proof. move => ha hb. suff h: SCF [:: a, - b & l'] = SCF(a-1::1::b-1:: [seq -x | x <- l']). case lz: (l== nil);first by rewrite (eqP lz) h. by rewrite SCF_cat ?lz // SCF_cat ?lz // h. rewrite/= SCF'_opp SCF2_bis// !mul1r addrAC -addrA (addrC _ x) ; congr (_ + _). rewrite (addrAC b) (addrK (- 1) (b - x)). by rewrite subf_div2 // (addrC (b-x)) addrK mulN1r - invrN opprB. 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)