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