proposition: Lemma lta_distincts : forall A B C D E F, LtA A B C D E F -> A<>B /\ C<>B /\ D<>E /\ F<>E /\ D <> F.
proof: Proof. intros A B C D E F Hlta. assert (Hlea : LeA A B C D E F) by (destruct Hlta; assumption). apply lea_distincts in Hlea. spliter. repeat split; auto. intro. subst F. assert (Bet D E D) by (apply (col_lta__bet A B C); Col). treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2