proposition: Lemma absvec_abscisse : forall O I J M : PO, repere O I J -> absvec (vec O M) = abscisse M.
proof: Proof. intros. elim existence_coordonnees with (O := O) (I := I) (J := J) (M := M); [ intros x H0; elim H0; [ intros y H1; try clear H0; try exact H1 ] | auto ]. rewrite <- (absvec_def H H1); eauto with geo. Qed.