proposition: Lemma normr_unit : {homo (@norm _ R) : x / x \is a GRing.unit}.
proof: Proof. move=> x /= /unitrP [y [yx xy]]; apply/unitrP; exists `|y|. by rewrite -!normrM xy yx normr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)