proposition: Lemma Cplus_z_zeroC : forall z : C, Cplus z zeroC = 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 (Cplus_def (z1:=z) (z2:=zeroC) (x1:=x1) (y1:=y1) (x2:=0) (y2:=0)); auto. replace (x1 + 0) with x1; [ idtac | ring ]. replace (y1 + 0) with y1; [ auto | ring ]. Qed.