proposition: Lemma Cmod2_alt (c:C) : (Cmod c ^2 = Re c ^2 + Im c ^2)%R.
proof: Proof. unfold Cmod. rewrite <-Rsqr_pow2, Rsqr_sqrt. trivial. apply Rplus_le_le_0_compat; apply pow2_ge_0. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy