proposition: Lemma changes_itv_mods_cindex a b : a < b -> forall p q, all (fun p => ~~ root p a) (mods p q) -> all (fun p => ~~ root p b) (mods p q) -> changes_itv_mods a b p q = cindex a b q p.
proof: Proof. move=> hab p q. 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_itv_mods0p cindexpC. have p_neq0 : p != 0 by rewrite -(mods_eq0 p q) hrpq. move: hrpq IHs; rewrite neq0_mods_rec //. move=> [_ <-] IHs /= /andP[rpa Ha] /andP[rpb Hb]. move=> /(_ _ _ (erefl _) Ha Hb) in IHs. have [->|q_neq0] := eqVneq q 0; first by rewrite changes_itv_modsp0 cindex0p. move: Ha Hb; rewrite neq0_mods_rec //= => /andP[rqa _] /andP[rqb _]. rewrite cindex_rec 1?changes_itv_mods_rec; by rewrite ?rootM ?negb_or ?rpa ?rpb ?rqa ?rqb // IHs. 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)