proposition: Lemma schangei_opp l: schange_index l = schange_index (opp_seq l).
proof: Proof. rewrite /schange_index - {2}oppr0; move: 0 0%N; elim: l; first by done. by move => a l hrec y n /=; rewrite mulrNN - hrec - hrec ! oppr_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol