proposition: Lemma l11_41_aux : forall A B C D, ~ Col A B C -> Bet B A D -> A <> D -> LtA A C B C A D.
proof: Proof. intros. assert(exists M , Midpoint M A C). apply midpoint_existence. ex_and H2 M. double B M P. assert(Cong_3 A C B C A P). repeat split. apply cong_pseudo_reflexivity. eapply l7_13. apply l7_2. apply H3. apply l7_2. assumption. eapply l7_13. apply H3. apply l7_2. assumption. assert(A <> C). intro. subst C. apply H. apply col_trivial_3. assert(B <> C). intro. subst C. apply H. apply col_trivial_2. assert(C <> D). intro. subst C. apply H. apply col_permutation_4. apply bet_col. assumption. assert(A <> M). intro. subst M. apply is_midpoint_id in H3. contradiction. assert(CongA A C B C A P). apply cong3_conga; assumption. assert(exists X, Bet A X P /\ Bet M X D). eapply inner_pasch. apply between_symmetry. apply H0. apply midpoint_bet. apply l7_2. assumption. ex_and H10 X. split. unfold LeA. exists P. split. assert(InAngle P M A D). repeat split. auto. auto. intro. subst P. unfold CongA in H9. spliter. absurde. exists X. split. assumption. right. apply bet_out. intro. subst X. apply H. eapply (col_transitivity_1 _ M). assumption. eapply (col_transitivity_1 _ D). assumption. apply col_permutation_1. apply bet_col. assumption. apply col_permutation_1. apply bet_col. assumption. apply bet_col. apply midpoint_bet. assumption. assumption. eapply l11_25. apply H12. apply l6_6. apply bet_out. auto. auto. apply midpoint_bet. assumption. apply out_trivial. auto. apply out_trivial. unfold CongA in H9. spliter. auto. assumption. intro. assert(CongA C A D C A P). eapply conga_trans. apply conga_sym. apply H12. assumption. assert (Coplanar C A D P). assert_diffs. apply coplanar_perm_3, col_cop__cop with B; Col. exists M. right. left. split; Col. apply conga_cop__or_out_ts in H13; trivial. induction H13. apply H. assert(Col B A P). apply col_permutation_2. apply (col_transitivity_1 _ D). assumption. apply out_col. assumption. apply col_permutation_1. apply bet_col. assumption. assert(B <> P). intro. subst P. apply l7_3 in H2. subst M. apply H. apply bet_col. apply midpoint_bet. assumption. assert(Col M B A). apply col_permutation_2. apply (col_transitivity_1 _ P). assumption. apply col_permutation_5. assumption. apply col_permutation_5. apply bet_col. apply midpoint_bet. assumption. eapply col_transitivity_1. apply H8. apply col_permutation_2. assumption. apply bet_col. apply midpoint_bet. assumption. assert(TS A C B P). repeat split. intro. apply H. apply col_permutation_4. assumption. intro. apply H. assert(Col M C P). apply col_permutation_2. apply (col_transitivity_1 _ A). auto. apply col_permutation_3. assumption. apply col_permutation_2. apply bet_col. apply midpoint_bet. assumption. assert(Col M B C). apply (col_transitivity_1 _ P). intro. subst M. apply l7_2 in H2. apply is_midpoint_id in H2. subst P. apply H. apply col_permutation_4. assumption. apply col_permutation_1. apply bet_col. apply midpoint_bet. assumption. apply col_permutation_5. assumption. apply col_permutation_1. apply (col_transitivity_1 _ M). intro. subst M. apply l7_2 in H3. apply is_midpoint_id in H3. subst C. absurde. apply col_permutation_3. apply bet_col. apply midpoint_bet. assumption. apply col_permutation_2. assumption. exists M. split. apply col_permutation_4. apply bet_col. apply midpoint_bet. assumption. apply midpoint_bet. assumption. assert(TS A C B D). repeat split. intro. apply H. apply col_permutation_4. assumption. intro. apply H. apply (col_transitivity_1 _ D). assumption. apply col_permutation_1. apply bet_col. assumption. apply col_permutation_4. assumption. exists A. split. apply col_trivial_1. assumption. assert(OS A C D P). unfold OS. exists B. split. apply l9_2. assumption. apply l9_2. assumption. apply invert_two_sides in H13. apply l9_9 in H13. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2