proposition: Lemma Cplus_algebrique : forall x1 y1 x2 y2 : R, Cplus (cons_cart x1 y1) (cons_cart x2 y2) = cons_cart (x1 + x2) (y1 + y2).
proof: Proof. intros. rewrite (Cplus_def (z1:=cons_cart x1 y1) (z2:=cons_cart x2 y2) (x1:=x1) (y1:=y1) (x2:=x2) (y2:=y2)); auto. Qed.