proposition: Lemma Cmod2_conj (c:C) : RtoC (Cmod c ^2) = c * Cconj c.
proof: Proof. rewrite Cmod2_alt. destruct c as (x,y). unfold Cconj, Cmult, RtoC. simpl. f_equal; ring. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy