proposition: Lemma normrMn x n : `|x *+ n| = `|x| *+ n.
proof: Proof. rewrite -mulr_natr -[RHS]mulr_natr normM. congr (_ * _); apply/eqP; rewrite -ge0_def. elim: n => [|n ih]; [exact: lerr | apply: (le_trans ih)]. by rewrite le_def -natrB // subSnn -[_%:R]subr0 -le_def mulr1n le01. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)