proposition: Theorem SegmTrisectExistence: forall A B, exists C, exists D, Bet_4 A C D B /\ Cong A C C D /\ Cong C D D B.
proof: Proof. assert(LEM1:forall A B D E F G, ~ Col B A E -> Col D F G -> Par F G E B -> ~ Par F G A B). { intros A0 B0 D0 E0 F0 G0. intros. intro. assert_all. assert(Par E0 B0 G0 F0). Par. assert(Par E0 B0 A0 B0) by (apply par_trans with G0 F0; auto). assert(Par B0 A0 B0 E0);finish. assert(Col B0 A0 E0). ColR. ColR. } intros. induction (eq_dec_points A B). - exists A. exists B. assert_all. split;finish. unfold Bet_4. split;finish. - assert(exists C, exists D, A <> D /\ Midpoint C A D /\ Midpoint D C B). { intros. assert(exists C, ~ Col A B C) by (apply not_col_exists; assumption). destruct H0 as [C]. Name D the symmetric of A wrt C. Name E the symmetric of C wrt D. assert(B <> E). { intro. subst. assert(Col A C E). ColR. ColR. } assert(exists F, exists G, Col D F G /\ Par F G E B). { intros. assert(exists F, exists G, F<>G /\ Par E B F G /\ Col D F G) by (apply parallel_existence; auto). destruct H4 as[F [G]]. spliter. exists F. exists G. Par. } destruct H4 as [F H5]. destruct H5 as [G]. assert_all. assert(A <> E). { intro. subst. assert(Cong C E D E). CongR. assert(C = D) by (apply between_cong with E;finish). CongR. } assert(~ Col B A E). { intro. assert(Col A C E) by (apply l6_16_1 with D;finish). assert(Col A E C);Col. assert(Col A E B). { assert(Col A B C). ColR. Col. } assert(Col A C B). ColR. Col. } assert(~ Par F G A B). { intro. assert_all. assert(Par E B G F). Par. assert(Par E B A B) by (apply par_trans with G F;assumption). assert(Par B A B E);finish. assert(Col B A E). ColR. ColR. } assert(exists H, Col H F G /\ Col H A B) by (apply not_par_inter_exists; auto). destruct H14 as [HH]. spliter. assert(D <> HH). { intro. subst. assert(Col B A C). ColR. Col. } assert(Par D HH E B). { assert(Par E B F G). Par. assert(Par E B D HH). { apply par_col2_par with F G. assumption. assumption. Col. Col. } Par. } assert(exists I, Midpoint I A HH). apply midpoint_existence. destruct H19 as [I]. assert(Col I A HH);finish. assert(Par C I B E). { assert(Midpoint C D A);finish. assert(Midpoint I HH A);finish; assert(Par D HH C I) by (apply triangle_mid_par with A; finish). apply par_trans with D HH. + apply par_symmetry; auto. + Par. } assert(Par D HH B E). Par. assert(A <> HH). { intro. subst. assert(Col C HH D);finish. assert(I = HH) by (apply l7_3;auto). subst. assert_all. assert(Col D C HH);finish. assert(Col D C E);Col. assert(Col D HH E). ColR. assert(~ Col B HH D). { intro. assert(Col HH D B);Col. assert(Col HH D C);Col. assert(Col HH B C). ColR. auto. } assert(Inter HH D B E E). { unfold Inter. split;auto. split. assert(Col B B E);Col. exists B;auto. split;Col. } assert(~ Par HH D B E) by (apply inter__npar with E;auto). Par. } assert(Midpoint I A HH);finish. assert(Midpoint HH I B). { assert_all. assert(Par C I B E). Par. assert(Par D HH B E). Par. assert(Col HH A B);Col. assert(A <> HH). { intro. subst. assert(Col C HH D);finish. } assert(B <> I). { intro. subst. assert(Col A I C). ColR. Col. } auto. apply sesamath_4ieme_G2_ex47 with C D E. + assert(~ Col E C B). intro. assert(Col A B C); ColR. ColR. + intro. assert(Col B A C). ColR. Col. + ColR. + auto. + assert(Par B E D HH). Par. apply par_trans with B E; auto. + Par. } exists I. exists HH. auto. } destruct H0 as [C [D]]. exists C. exists D. spliter. split. unfold Bet_4. split;finish. split;finish. split;finish. unfold Midpoint in H1. destruct H1. unfold Midpoint in H2. destruct H2. apply outer_transitivity_between2 with C;auto. assert(C <> D). { intro. subst. assert(D = B). CongR. subst. assert(A = B). CongR. tauto. } auto. unfold Midpoint in H1. destruct H1. unfold Midpoint in H2. destruct H2. apply outer_transitivity_between with D;finish. assert(C <> D). { intro. subst. assert(D = B). CongR. subst. assert(A = B). CongR. tauto. } auto. split; finish. Qed.
imports: sesamath_exercises