proposition: Lemma leif_normC_Re_Creal z : `|'Re z| <= `|z| ?= iff (z \is real).
proof: Proof. rewrite -(mono_in_leif ler_sqr); try by rewrite qualifE /=. rewrite [`|'Re _| ^+ 2]normCK conj_Creal // normC2_Re_Im -expr2. rewrite addrC -leifBLR subrr (sameP (Creal_ImP _) eqP) -sqrf_eq0 eq_sym. by apply: leif_eq; rewrite -realEsqr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)