proposition: Lemma schangei_s0 l1 l2: all_eq0 l1 -> schange_index (l1 ++ l2) = SIA l2 (size l1) 0.
proof: Proof. elim l1 => // a l hrec /= /andP [/eqP -> /hrec]. rewrite /schange_index /= mul0r eqxx ltxx andbF orbF. by rewrite - addn1 - (addn1 (size l)) ! schangei_addm => <-. 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)