proposition: Lemma ltp__lep_neq : forall O E E' A B, LtP O E E' A B -> LeP O E E' A B /\ A <> B.
proof: Proof. intros. unfold LeP. split. left; auto. unfold LtP in H. ex_and H D. intro. subst B. assert(HD:= H). unfold Diff in HD. ex_and HD B'. unfold Sum in H2. unfold Ar2 in H2. spliter. clear H3. assert(Diff O E E' A A O). apply diff_null; auto. assert(D = O). apply (diff_uniqueness O E E' A A); auto. subst D. unfold Ps in H0. unfold Out in H0. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order