proposition: Lemma eqC_semipolar x y : `|x| = `|y| -> 'Re x = 'Re y -> 0 <= 'Im x * 'Im y -> x = y.
proof: Proof. move=> eq_norm eq_Re sign_Im. rewrite [x]Crect [y]Crect eq_Re; congr (_ + 'i * _). have /eqP := congr1 (fun z => z ^+ 2) eq_norm. rewrite !normC2_Re_Im eq_Re (can_eq (addKr _)) eqf_sqr => /pred2P[] // eq_Im. rewrite eq_Im mulNr -expr2 oppr_ge0 real_exprn_even_le0 //= in sign_Im. by rewrite eq_Im (eqP sign_Im) oppr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)