proposition: Lemma leif_Re_Creal z : 'Re z <= `|z| ?= iff (0 <= z).
proof: Proof. have ubRe: 'Re z <= `|'Re z| ?= iff (0 <= 'Re z). by rewrite ger0_def eq_sym; apply/leif_eq/real_ler_norm. congr (_ <= _ ?= iff _): (leif_trans ubRe (leif_normC_Re_Creal z)). apply/andP/idP=> [[zRge0 /Creal_ReP <- //] | z_ge0]. by have Rz := ger0_real z_ge0; rewrite (Creal_ReP _ _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)