proposition: Lemma modsp0 p : mods p 0 = if p == 0 then [::] else [::p].
proof: Proof. by rewrite mods_rec mods0p. 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)