proposition: Lemma lta_suppa2__lta : forall A B C D E F A' B' C' D' E' F', SuppA A B C A' B' C' -> SuppA D E F D' E' F' -> LtA A B C D E F -> LtA D' E' F' A' B' C'.
proof: Proof. unfold SuppA. intros; spliter. ex_and H3 A0. ex_and H2 D0. apply (conga_preserves_lta F E D0 C B A0); [apply conga_sym; assumption..|]. apply conga_distinct in H4. apply conga_distinct in H5. spliter. apply lta_comm, bet2_lta__lta with A D; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2