proposition: Lemma Cdiv_conj (a b : C) : b<>0 -> Cconj (a/b) = Cconj a / Cconj b.
proof: Proof. intros H. unfold Cdiv. now rewrite Cmult_conj Cinv_conj. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy