proposition: Lemma SegmTrisectSecondThirdUniqueness: forall A B C D, SecondThird C A B -> SecondThird D A B -> C = D.
proof: Proof. intros. unfold SecondThird in *. spliter. Name M1 the midpoint of A and C. Name M2 the midpoint of A and D. unfold Midpoint in *. spliter. assert(Bet A M1 C). Between. assert(Bet M1 C B). apply between_exchange3 with A;auto. assert(Bet A C B). auto. assert(Bet A M1 B). apply between_exchange4 with C; auto. assert(Bet A M2 D). Between. assert(Bet M2 D B). apply between_exchange3 with A;auto. assert(Bet A D B). auto. assert(Bet A M2 B). apply between_exchange4 with D; auto. assert(Cong A M1 C B). apply H2. split; auto. assert(Cong A M2 D B). apply H1. split;auto. assert(Bet_4 A M1 C B). unfold Bet_4. repeat split;auto. assert(Bet_4 A M2 D B). unfold Bet_4. repeat split;auto. assert(Bet A M2 D /\ Cong A M2 M2 D). split;auto. assert(Bet A M1 C /\ Cong A M1 M1 C). split;auto. eapply SegmTrisectUniqueness. split. apply H17. split. auto. split. assert(Cong M1 C C B). apply cong_inner_transitivity with A M1. apply H6. apply H15. auto. assert(Bet_4 A M2 D B). unfold Bet_4. repeat split;auto. split. apply H21. split. assert(Cong A M2 M2 D). CongR. auto. CongR. Qed.
imports: sesamath_exercises