proposition: Lemma Cplus_conj a b : Cconj (a+b) = Cconj a + Cconj b.
proof: Proof. destruct a as (xa,ya), b as (xb,yb). unfold Cplus, Cconj. simpl. f_equal. ring. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy