proposition: Lemma unicite_composantes_vecteur : forall (a1 a2 b1 b2 : R) (O I J A B : PO), repere O I J -> vec A B = add_PP (mult_PP a1 (vec O I)) (mult_PP a2 (vec O J)) :>PP -> vec A B = add_PP (mult_PP b1 (vec O I)) (mult_PP b2 (vec O J)) :>PP -> a1 = b1 :>R /\ a2 = b2 :>R.
proof: Proof. intros. elim existence_representant_vecteur with (A := O) (B := A) (C := B); [ intros D H2; try clear existence_representant_vecteur; try exact H2 ]. rewrite <- H2 in H0. rewrite <- H2 in H1. apply (unicite_coordonnees (O:=O) (I:=I) (J:=J) (M:=D) (x:=a1) (y:=a2) (x':=b1) (y':=b2)); auto. Qed.