proposition: Lemma schangei_Sn l n a: SIA l n.+1 a = [seq z.+1 | z <- SIA l n a].
proof: Proof. move: n a; elim: l => [ n z // | a l hrec n y /=]. by case hyp: ((y == 0) && (a != 0) || (a * y < 0))=> //=; rewrite hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol