proposition: Lemma re_le_Cmod (c:C) : Rabs (Re c) <= Cmod c.
proof: Proof. rewrite <- (Rabs_right (Cmod c)) by (apply Rle_ge; apply Cmod_ge_0). apply Rsqr_le_abs_0. rewrite !Rsqr_pow2 Cmod2_alt. rewrite <- (Rplus_0_r (Re c ^2)) at 1. apply Rplus_le_compat_l. rewrite <- Rsqr_pow2. apply Rle_0_sqr. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy