proposition: Lemma Cplus_associative : forall z1 z2 z3 : C, Cplus z1 (Cplus z2 z3) = Cplus (Cplus z1 z2) z3.
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. elim existence_parties_relles_imaginaires with (z := z3); intros x3 H; elim H; intros y3 H2; try clear H; try exact H2. rewrite (Cplus_def (z1:=z1) (z2:=z2) (x1:=x1) (y1:=y1) (x2:=x2) (y2:=y2)); auto. rewrite (Cplus_def (z1:=cons_cart (x1 + x2) (y1 + y2)) (z2:=z3) (x1:= x1 + x2) (y1:=y1 + y2) (x2:=x3) (y2:=y3)); auto. rewrite (Cplus_def (z1:=z2) (z2:=z3) (x1:=x2) (y1:=y2) (x2:=x3) (y2:=y3)); auto. rewrite (Cplus_def (z1:=z1) (z2:=cons_cart (x2 + x3) (y2 + y3)) (x1:=x1) (y1:=y1) (x2:=x2 + x3) (y2:=y2 + y3)); auto. replace (x1 + (x2 + x3)) with (x1 + x2 + x3); [ idtac | ring ]. replace (y1 + (y2 + y3)) with (y1 + y2 + y3); [ auto | ring ]. Qed.