proposition: Lemma nlt__le : forall A B C D, ~ Lt A B C D -> Le C D A B.
proof: Proof. intros A B C D HNLt. destruct (le_cases A B C D); trivial. destruct (cong_dec C D A B). apply cong__le; assumption. exfalso. apply HNLt. split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col