proposition: Lemma schangei_s0n l1 a l2: a !=0 -> all_eq0 l1 -> schange_index (l1 ++a :: l2) = size l1 :: (SIA l2 (size l1).+1 a).
proof: Proof. by move => anz alz; rewrite (schangei_s0 _ alz) /= eqxx anz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol