proposition: Lemma cartvec_AB : forall (a1 a2 b1 b2 : R) (O I J A B : PO), repere O I J -> a1 = abscisse A :>R -> a2 = ordonnee A :>R -> b1 = abscisse B :>R -> b2 = ordonnee B :>R -> b1 + - a1 = absvec (vec A B) :>R /\ b2 + - a2 = ordvec (vec A B) :>R.
proof: Proof. intros. apply (unicite_composantes_vecteur (a1:=b1 + - a1) (a2:= b2 + - a2) (b1:=absvec (vec A B)) (b2:=ordvec (vec A B)) (O:=O) (I:=I) (J:=J) (A:=A) (B:=B)); auto. apply composantes_vecAB; auto. apply cartvec_def; auto. Qed.