proposition: Lemma thales : forall O E E' P A B C D A1 B1 C1 D1 AD, O <> E -> Col P A B -> Col P C D -> ~ Col P A C -> Pj A C B D -> Length O E E' P A A1 -> Length O E E' P B B1 -> Length O E E' P C C1 -> Length O E E' P D D1 -> Prodg O E E' A1 D1 AD -> Prodg O E E' C1 B1 AD.
proof: Proof. intros. induction(col_dec O E E'). unfold Prodg. right. split. intro. unfold Ar2 in H10. spliter. contradiction. unfold Prodg in H8. induction H8. unfold Prod in H8. spliter. unfold Ar2 in H8. spliter. contradiction. tauto. induction H8. induction(eq_dec_points P B). subst B. apply length_cong in H5. apply cong_symmetry in H5. apply cong_identity in H5. subst B1. unfold Pj in H3. induction H3. induction H3. apply False_ind. apply H3. exists C. split; Col. spliter. apply False_ind. apply H2. ColR. subst D. apply length_cong in H7. apply cong_symmetry in H7. apply cong_identity in H7. subst D1. assert (AD = O). apply (prod_uniqueness O E E' A1 O). assumption. apply prod_0_r. assumption. unfold Prod in H8. spliter. unfold Ar2 in H3. tauto. subst AD. left. apply prod_0_r. assumption. unfold Length in H6. spliter. unfold LeP in H6. induction H6. unfold LtP in H6. ex_and H6 X. apply diff_sum in H6. unfold Sum in H6. spliter. unfold Ar2 in H6. tauto. subst C1; Col. induction(eq_dec_points A B). { subst B. induction H3. induction H3. apply False_ind. apply H3. exists A. split; Col. spliter. assert(C=D). apply(l6_21 P C A C); Col. subst D. assert(A1=B1). apply (length_uniqueness O E E' P A);auto. subst B1. assert(C1 = D1). apply (length_uniqueness O E E' P C);auto. subst D1. left. apply prod_comm. assumption. subst D. apply False_ind. apply H2; Col. } rename H11 into HAB. assert(Hl0:= H4). assert(Hl1:= H5). assert(Hl2:= H6). assert(Hl3:= H7). unfold Length in H4. unfold Length in H5. unfold Length in H6. unfold Length in H7. spliter. clean_duplicated_hyps. assert(exists C' : Tpoint, Cong_3 P A C O A1 C' /\ OS O A1 E' C'). { apply(l10_16 P A C O A1 E'); Cong. apply length_Ar2 in Hl0. induction Hl0. spliter. intro. induction(eq_dec_points A1 O). subst A1. apply cong_symmetry in H22. apply cong_identity in H22. subst A. apply H2. Col. apply H5. ColR. subst A1. intro. apply cong_symmetry in H22. apply cong_identity in H22. subst A. apply H2. Col. } ex_and H4 C1'. assert(CongA P A C O A1 C1'). { apply(cong3_conga). intro. subst A. apply H2; Col. intro. subst C. apply H2; Col. assumption. } assert(HN:~Col O C1 C1'). { intro. unfold OS in H5. ex_and H5 K. unfold TS in H23. spliter. apply H23. apply col_permutation_2. apply (col_transitivity_1 _ C1). intro. subst C1. treat_equalities. apply H2. Col. ColR. Col. } assert(HH:= midpoint_existence C1 C1'). ex_and HH M. assert(HH:= l10_2_existence O M D1). ex_and HH D1'. unfold Reflect in H23. induction H23. spliter. unfold ReflectL in H24. spliter. ex_and H24 N. assert(Out O C1 D1). { apply (length_out O E E' P C P D). intro. subst C. apply cong_identity in H16. subst C1. apply H2; Col. intro. subst D. apply cong_identity in H13. subst D1. assert(AD=O). { apply (prod_uniqueness O E E' A1 O). assumption. apply prod_0_r. unfold Prod in H8. spliter. unfold Ar2 in H8. tauto. Col. } subst AD. induction H3. induction H3. apply H3. exists A. split; Col. spliter. apply H2. ColR. subst B; tauto. assumption. assumption. } assert(Out O A1 C1). { apply (length_out O E E' P A P C). intro. subst A. apply cong_identity in H22. subst A1. apply H2; Col. intro. subst C. apply cong_identity in H16. subst C1. unfold Out in H27. tauto. assumption. assumption. } assert(M <> C1). { intro. subst M. eapply (symmetric_point_uniqueness _ _ C1) in H7. subst C1'. apply H2. apply out_col. apply(cong3_preserves_out O A1 C1 P A C H28). unfold Cong_3 in *. spliter. repeat split; Cong. apply l7_3_2. } assert(Per O M C1). { unfold Per. exists C1'. split. assumption. unfold Cong_3 in H4. spliter. apply (cong_transitivity _ _ P C); Cong. } apply per_perp_in in H30; auto. apply perp_in_comm in H30. apply perp_in_perp_bis in H30. assert(Out O C1' D1'). { apply(image_preserves_out O M O C1 D1). assumption. unfold Reflect. left. split; auto. unfold ReflectL. split. exists O. split; Midpoint; Col. right. auto. unfold Reflect. left. split; auto. unfold ReflectL. split. exists M. split; Midpoint; Col. left. induction H30. apply perp_sym. apply perp_comm. apply (perp_col _ M). intro. subst C1'. apply l7_3 in H7. contradiction. Perp. unfold Midpoint in H7. spliter. Col. apply perp_distinct in H30. tauto. unfold Reflect. left. split; auto. unfold ReflectL. split. exists N. split; Midpoint; Col. left. induction H25. apply perp_right_comm. assumption. subst D1'. apply l7_3 in H24. subst D1. induction H30. apply perp_not_col in H24. apply False_ind. apply H24. apply out_col in H27. apply col_permutation_2. apply (col_transitivity_1 _ N). intro. subst N. apply cong_symmetry in H13. apply cong_identity in H13. subst D. unfold Pj in H3. induction H3. induction H3. apply H3. exists A. split; Col. spliter. apply H2. ColR. subst B. tauto. Col. Col. apply perp_distinct in H24. tauto. } assert(Perp O N D1 N). { apply (perp_col O M D1 N). intro. subst N. apply HN. unfold Midpoint in H24. spliter. apply bet_col in H24. apply out_col in H31. apply out_col in H27. eapply (col_transitivity_1 _ D1'). intro. subst D1'. apply cong_identity in H32. subst D1. treat_equalities. induction H3. induction H1. apply H1. exists A. split; Col. spliter. apply H2. ColR. subst B. tauto. apply(col_transitivity_1 _ D1). intro. subst D1. treat_equalities. induction H3. induction H1. apply H1. exists A. split; Col. spliter. apply H2. ColR. subst B. tauto. Col. Col. ColR. apply perp_sym. apply (perp_col _ D1'). intro. subst N. unfold Midpoint in H24. spliter. treat_equalities. apply HN. apply out_col in H31. apply out_col in H27. apply (col_transitivity_1 _ D1). intro. subst D1. treat_equalities. induction H3. induction H1. apply H1. exists A. split; Col. spliter. apply H2. ColR. subst B. tauto. Col. Col. induction H25. Perp. subst D1'. apply l7_3 in H24. subst N. apply False_ind. apply out_col in H31. apply out_col in H27. apply HN. apply (col_transitivity_1 _ D1). intro. subst D1. treat_equalities. treat_equalities. induction H3. induction H1. apply H1. exists A. split; Col. spliter. apply H2. ColR. subst B. tauto. Col. Col. unfold Midpoint in H24. spliter. apply bet_col in H24. Col. Col. } apply perp_left_comm in H32. assert(Cong O D1 O D1'). { apply perp_perp_in in H32. apply perp_in_comm in H32. apply perp_in_per in H32. unfold Per in H32. ex_and H32 D2. assert(D2 = D1'). apply (l7_9 _ _ N D1); Midpoint. subst D2. assumption. } assert(Pj C1 C1' D1 D1'). { unfold Pj. left. induction H25; induction H30. apply (l12_9_2D _ _ _ _ O M). apply (perp_col _ M). intro. subst C1'. apply HN. Col. Perp. unfold Midpoint in H7. spliter. Col. Perp. apply perp_distinct in H30. tauto. subst D1'. apply l7_3 in H24. subst N. apply perp_distinct in H32. tauto. subst D1'. apply l7_3 in H24. subst N. apply perp_distinct in H32. tauto. } assert(Cong_3 P C A O C1' A1). { unfold Cong_3 in *. spliter. repeat split; Cong. } assert(CongA P C A O C1' A1). { apply cong3_conga. intro. subst C. apply H2. Col. intro. subst C. apply H2. Col. assumption. } unfold Cong_3 in H35. spliter. assert(Cong P A O A1 /\ (P <> A -> CongA C P A C1' O A1 /\ CongA C A P C1' A1 O)). { apply(l11_49 P C A O C1' A1); Cong. } spliter. assert(P <> A). { intro. subst A. apply H2. Col. } apply H40 in H41. clear H40. spliter. assert(CongA C A P D B P). { induction(bet_dec C P D). assert(Bet A P B). apply(project_preserves_bet A P A C C P D). assumption. unfold Proj. repeat split. intro. subst A. apply H2. Col. intro. subst C. apply H2. Col. intro. induction H43. apply H43. exists A. split; Col. spliter. apply H2. Col. Col. left. apply par_left_comm. apply par_reflexivity. intro. subst A. apply H2. Col. unfold Proj. repeat split. intro. subst A. apply H2. Col. intro. subst C. apply H2. Col. intro. induction H43. apply H43. exists A. split; Col. spliter. apply H2. Col. Col. right. reflexivity. unfold Proj. repeat split. intro. subst A. apply H2. Col. intro. subst C. apply H2. Col. intro. induction H43. apply H43. exists A. split; Col. spliter. apply H2. Col. Col. left. unfold Pj in H3. induction H3. apply par_symmetry. apply par_right_comm. assumption. subst D. apply False_ind. apply H2. ColR. assert(CongA C A B D B A <-> Par A C B D). apply(l12_21 A C B D). unfold TS. repeat split. intro. apply H2. ColR. intro. apply H2. assert(P <> D). intro. subst D. induction H3. induction H3. apply H3. exists A. split; Col. spliter. apply H3. apply (l6_21 P B A C); Col. intro. apply H2. ColR. subst B. tauto. ColR. exists P. split; Col. destruct H44. induction H3. assert(HH3:=H3). apply H45 in HH3. apply(l11_10 C A B D B A C P D P). assumption. apply out_trivial. intro. subst C. apply H2. Col. repeat split. intro. subst A. apply H2. Col. intro. subst B. tauto. left. assumption. apply out_trivial. intro. subst D. apply H2. ColR. repeat split. intro. subst B. apply H2. tauto. auto. left; Between. subst D. apply False_ind. apply H2. ColR. assert(Out P C D). unfold Col in H1. unfold Out. repeat split. intro. subst C. apply H42. Between. intro. subst D. apply H42. Between. induction H1. left; assumption. induction H1. right; Between. apply False_ind. apply H42. Between. assert(Out P A B). apply (project_preserves_out P C D P A B P A A C). assumption. intro. induction H44. apply H44. exists C. split; Col. spliter. contradiction. unfold Proj. repeat split. intro. subst A. apply H2. Col. intro. subst C. apply H2. Col. intro. induction H44. apply H44. exists A. split; Col. spliter. contradiction. Col. right. reflexivity. unfold Proj. repeat split. intro. subst A. apply H2. Col. intro. subst C. apply H2. Col. intro. induction H44. apply H44. exists A. split; Col. spliter. contradiction. Col. left. apply par_left_comm. apply par_reflexivity. intro. subst C. apply H2. Col. unfold Proj. repeat split. intro. subst A. apply H2; Col. intro. subst C. apply H2; Col. intro. induction H44. apply H44. exists A. split; Col. spliter. contradiction. Col. left. induction H3. apply par_left_comm. apply par_symmetry. assumption. subst D. apply False_ind. apply H2. ColR. apply (l12_22 A C B D P). assumption. apply out_one_side. left. assumption. assumption. induction H3. assumption. subst D. apply False_ind. apply H2. ColR. } assert(C <> A). { intro. subst C. unfold CongA in H42. tauto. } assert(P <> A). { intro. subst A. unfold CongA in H42. tauto. } assert(~Par P A C A). { intro. induction H45. apply H45. exists A. split; Col. spliter. apply H2. Col. } assert(CongA C P A D P B). { induction(bet_dec C P D). assert(Bet A P B). apply (project_preserves_bet P A C A C P D A P B); auto. repeat split; Col. left. right. repeat split; Col. repeat split; Col. repeat split; Col. unfold Pj in H3. induction H3. left. Par. right. auto. apply(l11_14 C P A D B); auto. intro. subst C. unfold CongA in H36. tauto. intro. subst D. induction H3. induction H3. apply H3. exists A. split; Col. spliter. apply H2. ColR. subst B. tauto. assert(Out P C D). apply(not_bet_out). Col. assumption. assert(Out P A B). apply(project_preserves_out P C D P A B P A C A). repeat split. intro. subst C. apply H46. Between. intro. subst D. apply H46. Between. unfold Out in H47. spliter. tauto. intro. induction H48. apply H48. exists C. split; Col. spliter. apply H2. Col. repeat split; Col. repeat split; Col. left. right. repeat split; Col. repeat split; Col. left. unfold Pj in H3. induction H3. Par. subst D. apply False_ind. unfold CongA in H42. tauto. apply conga_sym. apply out2__conga; auto. } assert(C1 <> C1'). { intro. subst C1'. apply HN. Col. } assert(O <> C1'). { intro. subst C1'. unfold CongA in H36. tauto. } assert(~Col O C1 C1'). { intro. induction H30. apply perp_not_col in H30. apply H30. unfold Midpoint in H7. spliter. apply bet_col in H7. ColR. apply perp_distinct in H30. tauto. } assert(~Par O C1' C1 C1'). { intro. induction H50. apply H50. exists C1'. split; Col. spliter. contradiction. } assert(~Par O C1 C1 C1'). { intro. induction H51. apply H51. exists C1. split; Col. spliter. contradiction. } assert(Out O C1' D1'). { apply(project_preserves_out O C1 D1 O C1' D1' O C1' C1 C1'); auto. repeat split; Col. repeat split; Col. left. Par. repeat split; Col. left. apply(l12_9_2D D1 D1' C1 C1' O M). assert(Perp D1 D1' N O). apply(perp_col D1 N N O D1'). intro. subst D1'. apply l7_3 in H24. subst N. apply perp_distinct in H32. tauto. Perp. unfold Midpoint in H24. spliter. apply bet_col in H24. Col. apply perp_sym. apply(perp_col O N D1 D1' M). assumption. Perp. Col. induction H30. apply (perp_col C1 M O M C1'); Col; Perp. unfold Midpoint in H7. spliter. apply bet_col in H7. Col. apply perp_distinct in H30. tauto. } assert(CongA C1' O A1 D1' O B1). { apply out2__conga. apply l6_6. assumption. apply(length_out O E E' P B P A B1 A1); auto. } assert(CongA D1' O B1 D P B). { apply (conga_trans _ _ _ C P A). apply (conga_trans _ _ _ C1' O A1). apply conga_sym. assumption. apply conga_sym. assumption. assumption. } assert((D1' <> B1 -> CongA O D1' B1 P D B /\ CongA O B1 D1' P B D)). { apply (l11_49 D1' O B1 D P B). assumption. apply (cong_transitivity _ _ O D1); Cong. assumption. } assert(D1' <> B1). { intro. subst D1'. induction H34. induction H34. apply H34. exists C1. split; Col. ColR. spliter. apply H49. ColR. subst D1. apply l7_3 in H24. subst N. apply perp_distinct in H32. tauto. } apply H55 in H56. spliter. clear H55. apply conga_comm in H57. assert(CongA C1' A1 O D1' B1 O <-> Par A1 C1' B1 D1'). { apply(l12_22 A1 C1' B1 D1' O). apply (length_out O E E' P A P B); auto. apply out_one_side. left. intro. apply H49. assert(A1 <> O). intro. subst A1. unfold CongA in H53. tauto. ColR. assumption. } destruct H55. assert(Par A1 C1' B1 D1'). { apply H55. apply (conga_trans _ _ _ D B P). apply (conga_trans _ _ _ C A P). apply conga_sym. assumption. assumption. apply conga_sym. assumption. } clear H55 H58. assert(Prod O C1 C1' A1 D1 B1). { unfold Prod. repeat split. assumption. ColR. ColR. ColR. exists D1'. repeat split. assumption. apply out_col in H31. ColR. left. Par. } assert(exists Y : Tpoint, Prod O E C1' A1 D1 Y /\ Prod O E C1' C1 B1 Y). { apply(prod_x_axis_unit_change O C1 C1' A1 D1 C1 B1 E). repeat split; Col. ColR. ColR. Col. exists B1. split; auto. apply prod_1_l; Col. ColR. } ex_and H58 Y. assert(HH:=prod_y_axis_change O E C1' E' A1 D1 Y H58 H9). { assert(Y = AD). apply(prod_uniqueness O E E' A1 D1); auto. subst Y. assert(HP:=prod_y_axis_change O E C1' E' C1 B1 AD H60 H9). left. assumption. } spliter. subst M. apply False_ind. unfold Midpoint in H7. spliter. apply bet_col in H7. Col. right. spliter. split. intro. apply H8. unfold Ar2 in H11. spliter. repeat split; Col. unfold Length in H4. tauto. unfold Length in H7. tauto. unfold Length in H7. tauto. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order