proposition: Lemma normD x y : le (norm (x + y)) (norm x + norm y).
proof: Proof. have sposM u v: lt 0 u -> le 0 (u * v) -> le 0 v. by rewrite /lt !posE normM andbC => /andP[/eqP-> /mulfI/inj_eq->]. have posD u v: le 0 u -> le 0 v -> le 0 (u + v). have [-> | nz_u u_ge0 v_ge0] := eqVneq u 0; first by rewrite add0r. by have /andP[]: lt 0 (u + v) by rewrite sposDl // /lt nz_u. have le_sqr u v: conj u = u -> le 0 v -> le (u ^+ 2) (v ^+ 2) -> le u v. case: (eqVneq u 0) => [-> //|nz_u Ru v_ge0]. have [u_gt0 | u_le0 _] := boolP (lt 0 u). by rewrite leB (leB u) subr_sqr mulrC addrC; apply: sposM; apply: sposDl. rewrite leB posD // posE normN -addr_eq0; apply/eqP. rewrite /lt nz_u posE -subr_eq0 in u_le0; apply: (mulfI u_le0). by rewrite mulr0 -subr_sqr normK Ru subrr. have pos_norm z: le 0 (norm z) by apply/posP; exists (sqrt z). rewrite le_sqr ?posJ ?posD // sqrrD !normK -normM rmorphD mulrDl !mulrDr. rewrite addrA addrC !addrA -(addrC (y * conj y)) !addrA. move: (y * _ + _) => u; rewrite -!addrA leB opprD addrACA {u}subrr add0r -leB. rewrite {}le_sqr ?posD //. by rewrite rmorphD !rmorphM /= !conjK addrC mulrC (mulrC y). rewrite -mulr2n -mulr_natr exprMn normK -natrX mulr_natr sqrrD mulrACA. rewrite -rmorphM (mulrC y x) addrAC leB mulrnA mulr2n opprD addrACA. rewrite subrr addr0 {2}(mulrC x) rmorphM mulrACA -opprB addrAC -sqrrB -sqrMi. apply/posP; exists (i * (x * conj y - y * conj x)); congr (_ * _). rewrite !(rmorphM, rmorphB) iJ !conjK mulNr -mulrN opprB. by rewrite (mulrC x) (mulrC y). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path bigop finset prime order ssralg) mathcomp(poly polydiv mxpoly generic_quotient countalg) mathcomp(ssrnum closed_field ssrint archimedean rat intdiv) mathcomp(algebraics_fundamentals)