proposition: Lemma not_and_lt : forall A B C D, ~ (Lt A B C D /\ Lt C D A B).
proof: Proof. intros A B C D. intro HInter. destruct HInter as [[Hle HNCong] []]. apply HNCong. apply le_anti_symmetry; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col