proposition: Lemma changes_itv_modsp0 a b p : changes_itv_mods a b p 0 = 0.
proof: Proof. rewrite /changes_itv_mods /changes_itv_poly modsp0 /changes_horner /=. by have [//|p_neq0 /=] := altP eqP; rewrite !mulr0 ltxx. 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)