proposition: Lemma Cinv_conj (a:C) : a<>0 -> Cconj (/a) = /Cconj a.
proof: Proof. intros H. assert (H' := H). apply Cmod_gt_0 in H'. rewrite <- sqrt_0 in H'. apply sqrt_lt_0_alt in H'. destruct a as (xa,ya). simpl in *. unfold Cinv, Cconj. simpl. rewrite !Rmult_1_r in H'. apply Rlt_not_eq in H'. f_equal; field; rewrite Rmult_opp_opp; now contradict H'. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy