proposition: Lemma conjCK : involutive (@conj_op C).
proof: Proof. have JE x : x^* = `|x|^+2 / x. have [->|x_neq0] := eqVneq x 0; first by rewrite rmorph0 invr0 mulr0. by apply: (canRL (mulfK _)) => //; rewrite mulrC -normCK. move=> x; have [->|x_neq0] := eqVneq x 0; first by rewrite !rmorph0. rewrite !JE normrM normfV exprMn normrX normr_id. rewrite invfM exprVn (AC (2*2) (1*(2*3)*4))/= -invfM -exprMn. by rewrite divff ?mul1r ?invrK // !expf_eq0 normr_eq0 //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)