proposition: Lemma points_distincts_non_zeroC : forall (z : C) (A B : PO), A <> B :>PO -> 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. apply nonorigine_image_nonzero with M; auto with geo. red in |- *; intros; apply H. apply vecteur_nul_conf. rewrite <- H1; rewrite H2; Ringvec. Qed.