proposition: Lemma normcE x : `|x| = sqrtc (x * x^*%C).
proof: Proof. case: x=> a b; simpc; rewrite [b * a]mulrC addNr sqrtc_sqrtr //. by simpc; rewrite /= addr_ge0 ?sqr_ge0. 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)