proposition: Lemma egalite_point_zeroC : forall (z : C) (A B : PO), A = B -> z = affixe_vec (vec A B) :>C -> z = zeroC :>C.
proof: Proof. intros z A B H; try assumption. elim existence_representant_vecteur with (A := O) (B := A) (C := B); intros M H1. rewrite <- H1; intros. cut (O = M); intros; auto. rewrite <- H2 in H0. rewrite affixe_origine; auto with geo. apply vecteur_nul_conf. rewrite H1; rewrite H; Ringvec. Qed.