proposition: Lemma Cplus_z_oppz : forall z : C, Cplus z (Copp z) = zeroC.
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. unfold zeroC in |- *; rewrite H0; rewrite Copp_algebrique; rewrite Cplus_algebrique. replace (x1 + - x1) with 0; [ idtac | ring ]. replace (y1 + - y1) with 0; [ auto | ring ]. Qed.