proposition: Lemma bet2_lta__lta : forall A B C D E F A' D', LtA A B C D E F -> Bet A B A' -> A' <> B -> Bet D E D' -> D' <> E -> LtA D' E F A' B C.
proof: Proof. intros A B C D E F A' D' Hlta. intros. assert (Hd := Hlta). apply lta_distincts in Hd. unfold LtA in *. spliter. split. apply (l11_36 A _ _ D); auto. intro. assert(CongA A B C D E F); auto. apply (l11_13 A' _ _ D'); try (apply conga_sym); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2