proposition: Lemma Conj_Copp : forall z : C, Conj (Copp z) = Copp (Conj z).
proof: Proof. intros. elim existence_parties_relles_imaginaires with (z := z); intros x1 H; elim H; intros y1 H0; try clear H; try exact H0. rewrite H0. rewrite Copp_algebrique. repeat rewrite Conj_algebrique. rewrite Copp_algebrique; auto. Qed.