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