proposition: Lemma l11_53 : forall A B C D, Per D C B -> C <> D -> A <> B -> B <> C -> Bet A B C -> LtA C A D C B D /\ Lt B D A D.
proof: Proof. intros. assert(A<>C) by (intro; treat_equalities; auto). spliter. assert(~ Col B A D). intro. assert(Col B C D). apply (col_transitivity_1 _ A); Col. assert(~Col B C D). apply per_not_col. auto. auto. apply l8_2. assumption. contradiction. assert(A <> D). intro. subst D. apply H5. apply col_trivial_2. assert(LtA C A D C B D). assert(HH:=l11_41 B A D C H5 H3 H2). spliter. assert(CongA C A D B A D). apply out2__conga. apply bet_out. auto. assumption. apply out_trivial. auto. eapply conga_preserves_lta. apply conga_sym. apply H9. apply conga_right_comm. apply conga_refl. intro. subst D. apply H5. apply col_trivial_3. auto. assumption. split. assumption. unfold Per in H. ex_and H B'. unfold Midpoint in H. spliter. assert(HH:= H8). assert(~Col B D B'). intro. apply H5. apply (col_transitivity_1 _ B'). intro. subst B'. apply between_identity in H. contradiction. apply (col_transitivity_1 _ C). assumption. apply bet_col. assumption. Col. Col. destruct(l11_44_1 B D B'). assumption. apply H12 in H8. destruct(l11_44_2 A D B'). intro. apply H10. apply col_permutation_1. apply (col_transitivity_1 _ A). intro. subst B'. apply between_symmetry in H3. assert(B = C). apply (between_equality _ _ A); assumption. contradiction. apply col_permutation_1. eapply (col_transitivity_1 _ C). assumption. Col. Col. Col. assert(LtA C A D C B' D). apply (conga_preserves_lta C A D C B D). apply conga_refl. auto. auto. apply conga_sym. apply l11_10 with B D B' D. apply conga_sym in H8. apply conga_comm in H8. apply H8. apply bet_out. intro. subst B'. apply cong_identity in H9. contradiction. apply between_symmetry. assumption. apply out_trivial. intro. subst B'. apply H10. apply col_trivial_2. apply bet_out; auto. apply out_trivial. intro. subst D. apply H10. apply col_trivial_1. assumption. assert(B' <> A). intro. subst B'. apply between_symmetry in H3. assert(B=C). eapply between_equality. apply H. assumption. contradiction. assert (Lt D B' D A). apply l11_44_2_b. apply (conga_preserves_lta D A C D B' C). apply out2__conga. apply out_trivial. auto. apply l6_6. apply bet_out. auto. eapply outer_transitivity_between2. apply H3. assumption. auto. apply out2__conga. apply out_trivial. intro. subst B'. apply H10. apply col_trivial_2. apply l6_6. apply bet_out. intro. subst B'. apply cong_identity in H9. contradiction. eapply outer_transitivity_between. apply between_symmetry. apply H. apply between_symmetry. assumption. auto. apply lta_comm. assumption. unfold Lt in H17. spliter. unfold Lt. split. eapply l5_6. apply H17. Cong. apply cong_pseudo_reflexivity. intro. apply H18. eapply cong_transitivity. apply cong_symmetry. apply HH. apply cong_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2