proposition: Lemma unicite_coordonnees : forall (O I J M : PO) (x y x' y' : R), repere O I J -> vec O M = add_PP (mult_PP x (vec O I)) (mult_PP y (vec O J)) -> vec O M = add_PP (mult_PP x' (vec O I)) (mult_PP y' (vec O J)) -> x = x' /\ y = y'.
proof: Proof. unfold vec, repere in |- *; intros. deroule_triangle O I J. cut (cons 1 M = add_PP (add_PP (cons x I) (cons y J)) (cons (1 + - (x + y)) O)); intros. apply unicite_coor_bar2 with (2 := H6); auto. auto with geo. RingPP2 H1. RingPP. RingPP2 H0. RingPP. Qed.