proposition: Lemma position_3points_2: forall (A B C :PO), orient A B C \/ orient B A C \/ alignes A B C.
proof: Proof. intros A B C . destruct (@total_order_T (aire (vec A B)(vec A C)) 0) as [[H | H ] |H]. right;left. apply orient_cycle;apply orient_cycle. unfold orient. rewrite aire_anti_symetrique;lra. elim (classic (A=B));intros H0. right;right. rewrite H0;auto with geo. destruct (@aire_nulle_colineaires A B A C H0 H) as [k H1]. right;right. apply colineaire_alignes with (k:=k);auto. left. unfold orient;auto. Qed.