proposition: Lemma schange_cat l1 a l2: a != 0 -> schange (l1++a::l2) = (schange (l1++[::a]) + schange (a::l2)) %N.
proof: Proof. move => anz. rewrite /schange /filter0 filter_cat cats1 filter_rcons anz. set w := [seq z <- a :: l2 | z != 0]. elim [seq z <- l1 | z != 0]; first by rewrite /= mulr0 ltxx. move => b l /= ->. rewrite - addnA. congr addn. by rewrite -cats1 /w; case l => //=; rewrite anz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)