proposition: Lemma changes_itv_mods0p a b q : changes_itv_mods a b 0 q = 0.
proof: Proof. by rewrite /changes_itv_mods /changes_itv_poly mods0p /changes_horner /= subrr. 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)