proposition: Lemma invc_norm (x : R[i]) : x^-1 = `|x|^-2 * x^*%C.
proof: Proof. case: (altP (x =P 0)) => [->|dx]; first by rewrite rmorph0 mulr0 invr0. apply: (mulIf dx); rewrite mulrC divff // -mulrA [_^*%C * _]mulrC -(sqr_normc x). by rewrite mulVf // expf_neq0 ?normr_eq0. 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)