proposition: Lemma mu0 x : \mu_x 0 = 0%N.
proof: Proof. by rewrite /multiplicity {1}eqxx. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)