proposition: Lemma normcV x : normc x^-1 = (normc x)^-1.
proof: Proof. have [->|x0] := eqVneq x 0; first by rewrite ?(invr0,normc0). have nx0 : normc x != 0 by apply: contra x0 => /eqP/eq0_normc ->. by apply: (mulfI nx0); rewrite -normcM !divrr ?unitfE// normc1. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)