proposition: Lemma cart_point_complexe2 : forall (z : C) (a b : R) (M : PO), vec O M = add_PP (mult_PP a (vec O I)) (mult_PP b (vec O J)) :>PP -> M = image z -> z = cons_cart a b.
proof: Proof. intros. eauto with geo. Qed.