proposition: Lemma changes_modsp0 p : changes_mods p 0 = 0.
proof: Proof. rewrite /changes_mods /changes_poly modsp0; have [//|p_neq0] := altP eqP. by rewrite /changes_minfty /changes_pinfty /= !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)