proposition: Lemma SCF_neg2 a b l : b != 1 -> b != 0 -> SCF (rcons (rcons l a) (-b)) = SCF(rcons (rcons (rcons l (a-1)) 1) (b-1)).
proof: Proof. move => ha hb. have ha': b - 1 - 0 != 0 by rewrite subr0 subr_eq0. have hb': b - 0 != 0 by rewrite subr0 . by move:(@SCF_neg1 a b l nil ha' hb'); rewrite /= - !cats1 - !catA. 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)