proposition: Lemma Cpow_conj a n : Cconj (a^n) = (Cconj a)^n.
proof: Proof. induction n; simpl. - unfold RtoC, Cconj. simpl. f_equal. ring. - rewrite Cmult_conj. now f_equal. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy