proposition: Fact normM : {morph norm : x y / x * y}.
proof: Proof. move=> x y /=; wlog x_ge0 : x / 0 <= x. by move=> IHx; case: (leN_total x) => /IHx//; rewrite mulNr !normN. wlog y_ge0 : y / 0 <= y; last by rewrite ?ge0_norm ?le0_mul. by move=> IHy; case: (leN_total y) => /IHy//; rewrite mulrN !normN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)