proposition: Lemma Conj_Conj : forall z : C, Conj (Conj z) = z.
proof: Proof. intros. elim existence_parties_relles_imaginaires with (z := z); intros x H; elim H; intros y H0; try clear H; try exact H0. rewrite H0. repeat rewrite Conj_algebrique. replace (- - y) with y; [ auto | ring ]. Qed.