proposition: Lemma orient_compensation : forall (A B C :PO), ~orient A B C \/ ~orient B A C.
proof: Proof. intros A B C. elim (classic (orient A B C));(intros H;auto). assert (H0 : orient B C A ) by (apply orient_cycle ;auto). right;red;intros H1. unfold orient in *. rewrite aire_anti_symetrique in H1. lra. Qed.