proposition: Lemma lta_trans : forall A B C A1 B1 C1 A2 B2 C2, LtA A B C A1 B1 C1 -> LtA A1 B1 C1 A2 B2 C2 -> LtA A B C A2 B2 C2.
proof: Proof. intros. assert(HH1:= H). assert(HH2:= H0). unfold LtA in H. unfold LtA in H0. spliter. assert(LeA A B C A2 B2 C2). eapply lea_trans. apply H. assumption. split. assumption. intro. assert(LtA A2 B2 C2 A1 B1 C1). eapply conga_preserves_lta. apply H4. apply conga_refl. unfold LeA in H0. ex_and H0 X. unfold CongA in H5. spliter. assumption. unfold LeA in H0. ex_and H0 X. unfold CongA in H5. spliter. assumption. assumption. apply (not_and_lta A1 B1 C1 A2 B2 C2). split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2