proposition: Lemma taq_taq_itv a b : a < b -> forall p q, all (fun p => p.[a] != 0) (mods p (p^`() * q)) -> all (fun p => p.[b] != 0) (mods p (p^`() * q)) -> taq (roots p a b) q = taq_itv a b p q.
proof: Proof. by move=> *; rewrite /taq_itv changes_itv_mods_cindex // taq_cindex. 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)