proposition: Lemma normCDeq x y : `|x + y| = `|x| + `|y| -> {t : C | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}.
proof: Proof. move=> lin_xy; apply: sig2_eqW; pose u z := if z == 0 then 1 else z / `|z|. have uE z: (`|u z| = 1) * (`|z| * u z = z). rewrite /u; have [->|nz_z] := eqVneq; first by rewrite normr0 normr1 mul0r. by rewrite normf_div normr_id mulrCA divff ?mulr1 ?normr_eq0. have [->|nz_x] := eqVneq x 0; first by exists (u y); rewrite uE ?normr0 ?mul0r. exists (u x); rewrite uE // /u (negPf nz_x); congr (_ , _). have{lin_xy} def2xy: `|x| * `|y| *+ 2 = x * y ^* + y * x ^*. apply/(addrI (x * x^* ))/(addIr (y * y^* )); rewrite -2!{1}normCK -sqrrD. by rewrite addrA -addrA -!mulrDr -mulrDl -rmorphD -normCK lin_xy. have def_xy: x * y^* = y * x^*. apply/eqP; rewrite -subr_eq0 -[_ == 0](@expf_eq0 _ _ 2). rewrite (canRL (subrK _) (subr_sqrDB _ _)) opprK -def2xy exprMn_n exprMn. by rewrite mulrN (@GRing.mul C).[AC (2*2) (1*4*(3*2))] -!normCK mulNrn addNr. have{def_xy def2xy} def_yx: `|y * x| = y * x^*. by apply: (mulIf nz2); rewrite !mulr_natr mulrC normrM def2xy def_xy. rewrite -{1}(divfK nz_x y) invC_norm mulrCA -{}def_yx !normrM invfM. by rewrite mulrCA divfK ?normr_eq0 // mulrAC mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)