proposition: Lemma ltP_neq : forall O E E' A B, LtP O E E' A B -> A <> B.
proof: Proof. intros. assert(HH:=ltP_ar2 O E E' A B H). unfold Ar2 in HH. spliter. unfold LtP in H. intro. subst B. ex_and H OO. assert(OO=O). apply (diff_uniqueness O E E' A A). assumption. apply diff_null; Col. subst OO. unfold Ps in H4. unfold Out in H4. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod