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