proposition: Lemma schangei0 l: all_eq0 l <-> schange_index l = [::].
proof: Proof. split; first by move /schangei_s0 => h; move: (h [::]); rewrite /= cats0. suff: forall l n, SIA l n 0 = [::] -> all_eq0 l by apply. elim => [ // | a l' hrec n]. by rewrite /= eqxx mulr0 ltxx orbF andTb; case az: (a==0) => //= /hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol