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