proposition: Lemma ltp__ltps: forall O E E' A B, LtP O E E' A B -> LtPs O E E' A B.
proof: Proof. intros. unfold LtP in H. ex_and H D. unfold LtPs. exists D. split; auto. apply diff_sum. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order