proposition: Lemma composantes_vecAB : forall (a1 a2 b1 b2 : R) (O I J A B : PO), repere O I J -> a1 = abscisse A -> a2 = ordonnee A -> b1 = abscisse B -> b2 = ordonnee B -> vec A B = add_PP (mult_PP (b1 + - a1) (vec O I)) (mult_PP (b2 + - a2) (vec O J)) :>PP.
proof: Proof. intros. generalize (cart_def (O:=O) (I:=I) (J:=J) (M:=A) (x:=a1) (y:=a2)); intros. generalize (cart_def (O:=O) (I:=I) (J:=J) (M:=B) (x:=b1) (y:=b2)); intros. replace (vec A B) with (add_PP (vec O B) (mult_PP (-1) (vec O A))); [ idtac | Ringvec ]. rewrite H4; auto. rewrite H5; auto. Ringvec. Qed.