proposition: Lemma unicite_coor_bar : forall (k k' : R) (A B I : PO), A <> B -> cons 1 I = add_PP (cons k A) (cons (1 + - k) B) -> cons 1 I = add_PP (cons k' A) (cons (1 + - k') B) -> k = k'.
proof: Proof. intros. elim produit_vecteur_nul with (a := k + - k') (A := A) (B := B); [ intros H2; try clear produit_vecteur_nul; try exact H2 | intros H2; try clear produit_vecteur_nul | try clear produit_vecteur_nul ]. RReplace k (k + - k' + k'). rewrite H2. ring. absurd (A = B); auto. VReplace (mult_PP (k + - k') (vec A B)) (add_PP (add_PP (cons k' A) (cons (1 + - k') B)) (add_PP (cons (- k) A) (cons (-1 + k) B))). rewrite <- H1. rewrite H0. RingPP. Qed.