proposition: Lemma unicite_coor_bar2 : forall (A B C I : PO) (x y x' y' : R), ~ alignes A B C -> cons 1 I = add_PP (add_PP (cons x A) (cons y B)) (cons (1 + - (x + y)) C) :>PP -> cons 1 I = add_PP (add_PP (cons x' A) (cons y' B)) (cons (1 + - (x' + y')) C) :>PP -> x = x' :>R /\ y = y' :>R.
proof: Proof. intros. assert (~ x <> x' /\ ~ y <> y'). apply not_or_and; auto. contrapose H. apply (unicite_coor_bar_aux (A:=A) (B:=B) (C:=C) (I:=I) (x:=x) (y:=y) (x':=x') (y':=y')); auto. elim H2; [ intros H3 H4; try clear H2; try exact H3 ]. split; (apply NNPP; auto). Qed.