proposition: Theorem SegmTrisectUniqueness: forall A B C D C' D', Bet_4 A C D B /\ Cong A C C D /\ Cong C D D B /\ Bet_4 A C' D' B /\ Cong A C' C' D' /\ Cong C' D' D' B -> (C = C' /\ D = D').
proof: Proof. assert(LEM0: forall A B C D C' D', A <> B -> Midpoint C A D -> Midpoint D C B -> Midpoint C' A D' -> Midpoint D' C' B -> (C = C' /\ D = D')). { assert(LEM1: forall A B C D C' D', A <> B -> Midpoint C A D -> Midpoint D C B -> Midpoint C' A D' -> Midpoint D' C' B -> C = C'). { assert(LEM2: forall A B C D C' D' B', A <> B -> ~ Col A B C'-> Midpoint C A D -> Midpoint D C B -> Midpoint C' A D' -> Midpoint D' C' B' -> Par D' D B' B /\ Par C' C B' B). { assert(LEM3: forall A B C D C' D' B', A <> B -> ~ Col A B C'-> Midpoint C A D -> Midpoint D C B -> Midpoint C' A D' -> Midpoint D' C' B' -> ~Par_strict C' B D D'). { intros. assert(Par D' D C' C). { assert(~ Col D D' A). { intro. assert(Col A D C'). ColR. Col. assert(A <> D). { intro. subst. ColR. } assert(Col D A B). ColR. assert(Col A B C'). ColR. Col. } apply (triangle_mid_par D' D A C C'). assert(D' <> D). { intro. subst. assert(Col A D C'). ColR. Col. } auto. assert(Midpoint C D A) by (apply l7_2;auto). auto. assert(Midpoint C' D' A) by (apply l7_2;auto). auto. } assert_all. assert(Coplanar C' B D D'). Cop. intro. assert(Par C' B D D') by (apply (par_strict_par);auto). assert(Par C' B C' C) by (apply par_trans with D D';auto). assert(Col C' B C) by (apply par_id;auto). assert(Col B C' A). ColR. Col. } intros. assert(C <> A). { intro. subst. assert(A = D). ColR. subst. assert(D = B). ColR. tauto. } assert_all. assert(Col C A B). ColR. assert(Par D' D C' C). { assert(~ Col D D' A). { intro. assert(Col A D C'). ColR. assert(A <> D). ColR. assert(Col D A B). ColR. assert(Col A B C'). ColR. Col. } apply (triangle_mid_par D' D A C C'). + intro. subst. assert(Col A D C'). ColR. Col. + apply l7_2;auto. + apply l7_2;auto. } assert_all. assert(Coplanar C' B D D'). Cop. assert(~ Par_strict C' B D D') by (apply LEM3 with A C B';auto). assert(exists X, Col X C' B /\ Col X D D') by (apply cop_npars__inter_exists;auto). destruct H9 as [X]. destruct H9. assert(Midpoint X B C'). { assert(Par D' D C' C). Par. assert(Par C' C D' D). Par. assert(Col D D' X). Col. assert(D <> X). { intro. subst. assert(Col B X C');Col. assert(C <> X). { assert_diffs. tauto. } assert(B <> X). { assert_diffs. auto. } assert(Col B C' A). ColR. assert(Col A B C');Col. } assert(~ Col C' B C). { intro. assert(Col B A C'). ColR. Col. } assert(Par C C' D D'). Par. assert(Par C C' D X) by (apply par_col_par with D'; auto). assert(Par D X C C'). Par. assert(Par X D C' C). Par. assert(~ Col C' C B). Col. assert(Midpoint D C B). auto. assert(Par C' C X D) by (apply par_symmetry; auto). assert(Midpoint X C' B) by (apply triangle_par_mid with C D; ColR). apply l7_2;auto. } assert(Midpoint D' B' C') by (apply l7_2;auto). assert(~ Col B' B C'). { intro. assert(Col C' A B). ColR. Col. } assert(Midpoint X B C');auto. assert(Midpoint D' B' C');auto. assert(Par_strict B' B D' X). apply GeoCoq.Tarski_dev.Ch13_1.triangle_mid_par with C';auto. assert(Par B' B D' X); Par. assert(Col D' X D); Col. assert(Par B' B D' D). apply par_col_par with X;auto. assert(Par D' D B' B); Par. assert(Par C' C B' B). { assert(Par D' D C' C); Par. assert(Par C' C D' D); Par. apply par_trans with D' D;auto. } tauto. } intros. assert(exists E, ~ Col A B E) by (apply not_col_exists; assumption). destruct H4 as [E]. Name F the symmetric of A wrt E. assert(Par F D E C). { assert(F <> D). { intro. subst. assert(Col A B E). ColR. tauto. } apply triangle_mid_par with A; auto. + apply l7_2;auto. + apply l7_2;auto. } assert(Par F D' E C'). { assert(F <> D'). { intro. subst. assert(Col A B E). ColR. tauto. } apply triangle_mid_par with A. + auto. + apply l7_2;auto. + apply l7_2;auto. } assert(~ Col E B F). { intro. assert(Col E B A). ColR. Col. } Name G the symmetric of E wrt F. assert(Par F D G B /\ Par E C G B) by (apply LEM2 with A;finish). assert(Par F D' G B /\ Par E C' G B) by (apply LEM2 with A;finish). spliter. assert(Par E C E C'). { apply par_trans with G B;auto. Par. } assert(Col E C C') by (apply par_id;auto). assert(C <> C' -> False). { intro. assert(Col E A B). { assert(Col C A B). { assert(C <> D). { intro. subst. assert(D = B) by (apply is_midpoint_id;auto). assert(D = A) by (apply is_midpoint_id_2;auto). subst. Col. } assert(Col C D A);finish. assert(Col C D B);finish. ColR. } assert(Col C' A B). { assert(C' <> D'). { intro. subst. assert(D' = B) by (apply is_midpoint_id;auto). assert(D' = A) by (apply is_midpoint_id_2;auto). subst. Col. } ColR. } ColR. } Col. } induction(eq_dec_points C C'). + auto. + tauto. } intros. split. + apply LEM1 with A B D D';auto. + apply LEM1 with B A C C' ;auto;finish. } intros. spliter. induction(eq_dec_points A B). + subst. split. unfold Bet_4 in *. spliter. assert_all. reflexivity. unfold Bet_4 in *. spliter. assert_all. reflexivity. + apply LEM0 with A B; finish. unfold Bet_4 in H. spliter. unfold Bet_4 in H2. spliter. unfold Midpoint. split;auto. unfold Bet_4 in H. spliter. unfold Bet_4 in H2. spliter. unfold Midpoint. split;auto. unfold Bet_4 in H. spliter. unfold Bet_4 in H2. spliter. unfold Midpoint. split;auto. unfold Bet_4 in H. spliter. unfold Bet_4 in H2. spliter. unfold Midpoint. split;auto. Qed.
imports: sesamath_exercises