proposition: Lemma changes_mods_cindex p q : changes_mods p q = cindexR q p.
proof: Proof. elim: mods {-2}p {-2}q (erefl (mods p q)) => [|r s IHs] {}p {}q hrpq. move/eqP: hrpq; rewrite mods_eq0 => /eqP ->. by rewrite changes_mods0p cindexRpC. rewrite changes_mods_rec cindexR_rec IHs //. by move: hrpq IHs; rewrite mods_rec; case: (p == 0) => // [] []. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)