proposition: Lemma re_alt (c:C) : RtoC (Re c) = (c + Cconj c)/2.
proof: Proof. destruct c as (x,y). unfold Cconj, RtoC, Cplus, Cdiv, Cmult. simpl. f_equal; field. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy