proposition: Lemma normrV : {in GRing.unit, {morph (@norm _ R) : x / x ^-1}}.
proof: Proof. move=> x ux; apply: (mulrI (normr_unit ux)). by rewrite -normrM !divrr ?normr1 ?normr_unit. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)