proposition: Lemma ltP_pos : forall O E E' A, LtP O E E' O A -> Ps O E A.
proof: Proof. intros. unfold LtP in H. ex_and H A'. assert(~Col O E E' /\ Col O E A). unfold Diff in H. ex_and H X. unfold Sum in H1. spliter. unfold Ar2 in H1. tauto. spliter. assert(HH:= diff_A_O O E E' A H1 H2). assert(A = A'). apply(diff_uniqueness O E E' A O A A'); assumption. subst A'. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order