proposition: Lemma nlea__lta : forall A B C D E F, ~ LeA A B C D E F -> A <> B -> B <> C -> D <> E -> E <> F -> LtA D E F A B C.
proof: Proof. intros A B C D E F HNlea. intros. split. - elim(lea_total D E F A B C); auto. intro; exfalso; auto. - intro. apply HNlea. apply conga__lea. apply conga_sym; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2