proposition: Lemma ltp__diff_pos : forall O E E' A B D, LtP O E E' A B -> Diff O E E' B A D -> Ps O E D.
proof: Proof. intros. unfold LtP in H. ex_and H D'. assert(D = D'). { apply (diff_uniqueness O E E' B A); auto. } subst D'. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order