proposition: Lemma normrMz m (x : R) : `|x *~ m| = `|x| *~ `|m|.
proof: Proof. by rewrite -mulrzl normrM -intr_norm mulrzl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)