proposition: Lemma mul_conjC_gt0 x : (0 < x * x^* ) = (x != 0).
proof: Proof. have [->|x_neq0] := eqVneq; first by rewrite rmorph0 mulr0. by rewrite -normCK exprn_gt0 ?normr_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)