proposition: Lemma le__nlt : forall A B C D, Le A B C D -> ~ Lt C D A B.
proof: Proof. intros A B C D HLe HLt. apply (not_and_lt A B C D); split; auto. split; auto. unfold Lt in *; spliter; auto with cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col