proposition: Lemma schangei_snn l i s: schange_index l = i::s -> exists l1 a l2, [/\ l = l1 ++a :: l2, a != 0, i = size l1, all_eq0 l1 & SIA l2 (size l1).+1 a = s].
proof: Proof. case alt: (all_eq0 l); first by move /schangei0:alt => -> //. move: (allPn (negbT alt)) => /hasP /has_split_eq [l1 [a [l2 [ -> az al0]]]]. rewrite (schangei_s0n _ az al0) => /eqP;rewrite eqseq_cons. by move => /andP [/eqP <- /eqP <-];exists l1, a, l2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol