proposition: Lemma nle__lt : forall A B C D, ~ Le A B C D -> Lt C D A B.
proof: Proof. intros A B C D HNLe. destruct (le_cases A B C D). contradiction. split; trivial. intro. apply HNLe. apply cong__le; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col