proposition: Lemma position_3points_1: forall (A B C :PO), (~ orient A B C /\ ~ orient B A C) \/ ~ alignes A B C.
proof: Proof. intros A B C. elim (classic (~ orient A B C /\ ~ orient B A C));(intros H;auto). right. elim (@not_and_or (~orient A B C)(~orient B A C));auto;intro H1. assert(orient A B C) by (apply NNPP;auto). red;intros H2. unfold orient in H0. assert ( aire (vec A B)(vec A C) = 0) by apply (@aire_alignement A B C H2) . lra. assert(orient B A C) by (apply NNPP;auto). red;intros H2. assert (alignes B A C);auto with geo. unfold orient in H0. assert ( aire (vec B A)(vec B C) = 0) by apply (@aire_alignement B A C H3) . lra. Qed.