proposition: Lemma l13_2 : forall A B C D E, TS A B C D -> Per B C A -> Per B D A -> Col C D E -> Perp A E C D -> CongA B A C D A E /\ CongA B A D C A E /\ Bet C E D.
proof: Proof. intros. assert(HH:= H). unfold TS in HH. assert(~ Col C A B). spliter. assumption. spliter. assert(C <> D). intro. subst D. assert(OS A B C C). apply one_side_reflexivity. assumption. apply l9_9 in H. contradiction. assert(exists C', CongA B A C D A C' /\ OS D A C' B). apply(angle_construction_1 B A C D A B). intro. apply H5. Col. intro. apply H6. Col. ex_and H9 E'. assert(A <> B /\ A <> C /\ A <> D). unfold CongA in H9. spliter; auto. spliter. assert(HH:=l11_22 C A E' B D A B E'). assert(HH1:=ts_per_per_ts A B C D H H0 H1). unfold TS in HH1. assert (~ Col A C D). spliter. assumption. spliter. ex_and H7 T. ex_and H17 T2. assert(T = T2). apply (l6_21 A B C D); Col. subst T2. assert(InAngle B D A C). unfold InAngle. repeat split; auto. exists T. split. Between. right. unfold Out. repeat split. intro. subst T. assert(~ Col C D A /\ Per A E D). apply(l8_16_1 C D A D E H2). Col. apply perp_sym. assumption. spliter. apply H20. Col. auto. left. assumption. assert(LeA C A B C A D). unfold LeA. exists B. split. apply l11_24. assumption. apply conga_refl; auto. assert(InAngle E' D A C). eapply lea_in_angle. apply lea_comm. eapply l11_30. apply H21. apply conga_comm. assumption. apply conga_refl; auto. assert(HH1:=ts_per_per_ts A B C D H H0 H1). assert(OS D A C B). apply ts_ts_os. apply invert_two_sides. assumption. apply l9_2. assumption. eapply one_side_transitivity. apply H22. apply one_side_symmetry. assumption. unfold InAngle in H22. spliter. ex_and H25 E''. induction H26. subst E''. apply False_ind. apply H15. apply bet_col in H25. Col. assert(CongA B A C D A E''). apply (l11_10 B A C D A E'); try apply out_trivial; auto. assert(A <> T). intro. subst T. apply H15. Col. induction(eq_dec_points E'' T). subst E''. apply l13_2_1; auto. eapply l11_10. apply conga_left_comm. apply H27. apply out_trivial; auto. apply out_trivial; auto. apply out_trivial; auto. unfold Out. repeat split; auto. assert(D <> E''). intro. subst E''. apply conga_sym in H27. apply eq_conga_out in H27. apply out_col in H27. apply H5. Col. assert(C <> E''). intro. subst E''. assert(OS C A B D). apply invert_one_side. apply ts_ts_os. assumption. apply ts_per_per_ts; auto. assert(Out A B D). apply(conga_os__out C A B D). apply conga_comm. assumption. assumption. apply out_col in H32. apply H6. Col. assert(A <> E''). intro. subst E''. unfold Out in H26. tauto. assert(~ Col E'' A B). intro. apply H29. apply bet_col in H25. apply (l6_21 A B C D); Col. assert(CongA C A E'' D A B). apply (l11_22 C A E'' B D A B E''). split. induction(one_side_dec A B C E''). right. split. auto. unfold OS. exists C. split. unfold TS. repeat split. auto. intro. apply H15. apply bet_col in H25. apply col_permutation_1. eapply (col_transitivity_1 _ E''); Col. intro. apply bet_col in H25. apply H15. apply col_permutation_2. eapply (col_transitivity_1 _ E''); Col. exists E''. split; Col. assert(TS A E'' T C). unfold TS. repeat split. auto. intro. apply H29. apply (l6_21 A B C D);Col. eapply (col_transitivity_1 _ T); Col. apply bet_col in H25. Col. intro. apply H15. ColR. exists E''. split. Col. assert(Bet C T E'' \/ Bet C E'' T). eapply l5_3. apply H18. Between. induction H35. assert(TS A B C E''). unfold TS. repeat split; auto. exists T. split. Col. auto. apply l9_9 in H36. contradiction. Between. eapply (l9_5 _ _ T _ A); Col. unfold Out. repeat split; auto. left. apply cop_nos__ts in H34; auto. split. auto. assert(OS A B D E''). eapply l9_8_1. apply l9_2. apply H. apply l9_2. assumption. assert(TS A E'' T D). unfold TS. repeat split. auto. intro. apply H33. apply col_permutation_2. apply(col_transitivity_1 _ T); Col. intro. apply bet_col in H25. apply H15. apply col_permutation_1. eapply (col_transitivity_1 _ E''); Col. exists E''. split. Col. assert(Bet D T E'' \/ Bet D E'' T). eapply l5_3. apply between_symmetry. apply H18. assumption. induction H36. assert(TS A B D E''). unfold TS. repeat split; auto. exists T. split; Col. apply l9_9 in H37. contradiction. Between. apply l9_2. eapply (l9_5 _ _ T _ A). auto. Col. unfold Out. repeat split; auto. apply col_cop__cop with D; Col; Cop. split. apply conga_left_comm. auto. apply conga_right_comm. apply conga_refl; auto. prolong B C C' B C. prolong B D D' B D. assert(Cong_3 B A D D' A D). apply l8_2 in H1. unfold Per in H1. ex_and H1 D''. assert(Midpoint D B D'). unfold Midpoint. split; Cong. assert(D' = D''). eapply symmetric_point_uniqueness. apply H40. auto. subst D''. repeat split; Cong. assert(CongA B A D D' A D). apply cong3_conga; auto. assert(Cong_3 B A C C' A C). apply l8_2 in H0. unfold Per in H0. ex_and H0 C''. assert(Midpoint C B C'). unfold Midpoint. split; Cong. assert(C' = C''). eapply symmetric_point_uniqueness. apply H42. auto. subst C''. repeat split; Cong. assert(CongA B A C C' A C). apply cong3_conga; auto. assert(CongA E'' A C' D' A E''). apply l11_22 with C D. split. clear HH. left. assert(OS C A D E''). eapply out_out_one_side. apply one_side_reflexivity. intro. apply H15. Col. unfold Out. repeat split; auto. right. Between. assert(OS C A B D). apply in_angle_one_side. intro. apply H15. Col. intro. apply H5. Col. apply l11_24. auto. assert(TS C A B C'). unfold TS. repeat split. auto. intro. apply H5. Col. intro. apply H5. apply bet_col in H35. assert(C <> C'). intro. subst C'. apply cong_symmetry in H36. apply cong_identity in H36. subst C. apply H16. Col. eapply (col_transitivity_1 _ C'); Col. exists C. split; Col. assert(OS C A B E''). eapply one_side_transitivity. apply H44. auto. assert(OS D A C E''). eapply out_out_one_side. apply one_side_reflexivity. intro. apply H15. Col. unfold Out. repeat split; auto. assert(OS D A B C). apply in_angle_one_side. intro. apply H15. Col. intro. apply H6. Col. auto. assert(TS D A B D'). unfold TS. repeat split. auto. intro. apply H6. Col. intro. apply H6. apply bet_col in H37. assert(D <> D'). intro. subst D'. apply cong_symmetry in H38. apply cong_identity in H38. subst D. apply H16. Col. eapply (col_transitivity_1 _ D'); Col. exists D. split; Col. assert(OS D A B E''). eapply one_side_transitivity. apply H48. auto. split. apply invert_two_sides. eapply l9_8_2. apply H45. auto. apply invert_two_sides. apply l9_2. eapply l9_8_2. apply H49. auto. split. eapply conga_trans. apply conga_comm. apply H34. apply H40. apply conga_sym. eapply conga_trans. apply conga_sym. apply H27. apply conga_right_comm. auto. assert(D' <> B). intro. subst D'. apply between_identity in H37. subst D. apply H16. Col. assert(C' <> B). intro. subst C'. apply between_identity in H35. subst C. apply H16. Col. assert(~ Col C' D' B). intro. apply H16. apply bet_col in H35. apply bet_col in H37. assert(Col C' B D). ColR. ColR. assert(Par_strict C' D' C D). apply(triangle_mid_par C' D' B D C). auto. unfold Midpoint. split. Between. Cong. unfold Midpoint. split. Between. Cong. assert(TS A E'' C D). unfold TS. repeat split. auto. intro. apply H15. apply bet_col in H25. apply col_permutation_2. eapply (col_transitivity_1 _ E''); Col. intro. apply H15. apply bet_col in H25. apply col_permutation_1. eapply (col_transitivity_1 _ E''); Col. exists E''. split; Col. Between. assert(TS B A C D). apply in_angle_two_sides. intro. apply H5. Col. intro. apply H6. Col. apply l11_24. assumption. assert (OS A B C C'). apply (out_one_side_1 _ _ _ _ B); Col. unfold Out. repeat split; auto. intro. subst C. apply H5. Col. assert (OS A B D D'). apply (out_one_side_1 _ _ _ _ B); Col. unfold Out. repeat split; auto. intro. subst D. apply H6. Col. apply invert_two_sides in H49. assert(TS A B C' D). eapply l9_8_2. apply H49. auto. assert(TS A B C' D'). apply l9_2. eapply l9_8_2. apply l9_2. apply H52. auto. assert(Perp C' D' A E''). apply cong_conga_perp. apply conga_right_comm in H43. apply conga_cop__or_out_ts in H43. induction H43. assert(OS A B C' D'). eapply (out_one_side_1 _ _ _ _ A); Col. intro. assert(B <> C'). intro. subst C'. apply H46. Col. apply H5. apply col_permutation_1. eapply col_transitivity_1. apply H55. apply bet_col in H35. Col. Col. apply l9_9 in H53. contradiction. apply invert_two_sides. assumption. apply coplanar_pseudo_trans with B C D; Cop. unfold Cong_3 in *. spliter. apply cong_transitivity with B A; Cong. apply conga_left_comm. assumption. assert(Cong A C' A B). apply l8_2 in H0. unfold Per in H0. ex_and H0 C''. assert(C' = C''). apply(symmetric_point_uniqueness B C C' C''); auto. split; Cong. subst C''. Cong. assert(Cong A D' A B). apply l8_2 in H1. unfold Per in H1. ex_and H1 D''. assert(D' = D''). apply(symmetric_point_uniqueness B D D' D''); auto. split; Cong. subst D''. Cong. assert(Cong A C' A D'). apply cong_transitivity with A B; Cong. assert(HM:=midpoint_existence C' D'). ex_and HM R. assert(exists X Y : Tpoint, Perp_at R X Y C' D' /\ Perp X Y D C /\ Coplanar C' D' B X /\ Coplanar C' D' B Y). apply l13_1_aux; auto. split; Between; Cong. split; Between; Cong. ex_and H59 X. ex_and H60 Y. assert(HXY:X <> Y). apply perp_distinct in H60. tauto. assert(Perp C D A E''). induction(eq_dec_points A R). subst R. assert(Perp_at A C' D' A E''). assert_cols. apply(l8_14_2_1b_bis C' D' A E'' A); Col. assert(Coplanar B C' D' E''). apply coplanar_pseudo_trans with B C D; Cop. assert(Coplanar C' D' X E''). apply coplanar_trans_1 with B; Col; Cop. assert(Coplanar C' D' Y E''). apply coplanar_trans_1 with B; Col; Cop. assert(Coplanar C' D' X A). exists A. left. split; Col. assert(Coplanar C' D' Y A). exists A. left. split; Col. assert(Col X Y A). apply(cop4_perp_in2__col X Y A E'' C' D' A); Perp. assert(Col X Y E''). apply(cop4_perp_in2__col X Y E'' A C' D' A); Perp. apply perp_sym. induction(eq_dec_points Y A). subst Y. apply(perp_col _ X). auto. Perp. Col. apply(perp_col _ Y). auto. apply perp_left_comm. apply (perp_col _ X); Col. Perp. ColR. assert(R <> C'). intro. subst R. unfold Midpoint in H58. spliter. apply cong_symmetry in H64. apply cong_identity in H64. subst D'. apply perp_distinct in H54. tauto. assert(Per A R C'). unfold Per. exists D'. split; auto. apply per_perp_in in H65; auto. apply perp_in_sym in H65. apply perp_in_perp_bis in H65. induction H65. apply perp_comm in H65. assert(Perp C' D' R A). apply(perp_col _ R). intro. subst D'. apply perp_distinct in H54. tauto. assumption. assert_cols. Col. assert(Perp_at R C' D' R A). apply(l8_14_2_1b_bis C' D' R A R); Col. assert_cols. Col. assert(Coplanar C' D' X A). apply coplanar_trans_1 with B; Cop; Col. assert(Coplanar C' D' Y A). apply coplanar_trans_1 with B; Cop; Col. assert(Coplanar C' D' X R). exists R. left. split; Col. assert(Coplanar C' D' Y R). exists R. left. split; Col. assert( Col X Y A). apply(cop4_perp_in2__col X Y A R C' D' R); Perp. assert( Col X Y R). apply(cop4_perp_in2__col X Y R A C' D' R); Perp. assert(Col A E'' R). apply(cop_perp2__col A E'' R C' D'); Perp. exists R. left. split; Col. assert(Col A R X). ColR. assert(Col A R Y). ColR. apply perp_sym. induction(eq_dec_points X A). subst X. apply (perp_col _ Y); Perp. ColR. apply (perp_col _ X); Col; Perp. apply perp_left_comm. apply(perp_col _ Y); Perp. ColR. apply perp_distinct in H65. tauto. assert(Col A E E''). apply cop_perp2__col with C D; Perp. exists E. left. split; Col. assert(E'' = E). apply (l6_21 C D A E); Col. apply perp_not_eq_1 in H3. assumption. subst E''. split. auto. split. apply conga_sym. apply conga_right_comm. auto. Between. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel