proposition: Lemma sposDl x y : lt 0 x -> le 0 y -> lt 0 (x + y).
proof: Proof. have sqrtJ z : le 0 z -> conj (sqrt z) = sqrt z. rewrite posE -{2}[z]sqrtK -subr_eq0 -mulrBr mulf_eq0 subr_eq0. by case/pred2P=> ->; rewrite ?rmorph0. case/andP=> nz_x /sqrtJ uJ /sqrtJ vJ. set u := sqrt x in uJ; set v := sqrt y in vJ; pose w := u + i * v. have ->: x + y = w * conj w. rewrite rmorphD rmorphM /= iJ uJ vJ mulNr mulrC -subr_sqr sqrMi opprK. by rewrite !sqrtK. apply/andP; split; last by apply/posP; exists w. rewrite -normK expf_eq0 //=; apply: contraNneq nz_x => /norm_eq0 w0. rewrite -[x]sqrtK expf_eq0 /= -/u -(inj_eq mul2I) !mulr2n -{2}(rmorph0 conj). by rewrite -w0 rmorphD rmorphM /= iJ uJ vJ mulNr addrACA subrr addr0. 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)