proposition: Lemma Conj_somme : forall z1 z2 : C, Conj (Cplus z1 z2) = Cplus (Conj z1) (Conj z2).
proof: Proof. intros. elim existence_parties_relles_imaginaires with (z := z1); intros x1 H; elim H; intros y1 H0; try clear H; try exact H0. elim existence_parties_relles_imaginaires with (z := z2); intros x2 H; elim H; intros y2 H1; try clear H; try exact H1. rewrite H1; rewrite H0. rewrite Cplus_algebrique. repeat rewrite Conj_algebrique. rewrite Cplus_algebrique. replace (- (y1 + y2)) with (- y1 + - y2); [ auto | ring ]. Qed.