proposition: Lemma lea__nlta : forall A B C D E F, LeA A B C D E F -> ~ LtA D E F A B C.
proof: Proof. intros. intro Hlta. destruct Hlta as [Hlea HNConga]. apply HNConga. apply lea_asym; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2