proposition: Lemma mods_eq0 p q : (mods p q == [::]) = (p == 0).
proof: Proof. by rewrite mods_rec; have [] := altP (p =P 0). 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)