proposition: Lemma absvec_ordvec_affixe : forall (a b : R) (A B : PO), a = absvec (vec A B) -> b = ordvec (vec A B) -> cons_cart a b = affixe_vec (vec A B).
proof: Proof. intros a b A B. elim existence_representant_vecteur with (A := O) (B := A) (C := B); intros D H1; try exact H1. rewrite <- H1; intros. apply affixe_point_vecteur. rewrite H0; rewrite H; rewrite (ordvec_ordonnee (O:=O) (I:=I) (J:=J) D); auto with geo. rewrite (absvec_abscisse (O:=O) (I:=I) (J:=J) D); auto with geo. Qed.