proposition: Lemma ltP_ar2 : forall O E E' A B, LtP O E E' A B -> Ar2 O E E' A B A.
proof: Proof. intros. unfold LtP in H. ex_and H D. apply diff_ar2 in H. unfold Ar2 in H. spliter. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod