proposition: Lemma SegmTrisectSecondThirdExistence: forall A B, exists T,SecondThird T A B.
proof: Proof. intros. assert (exists C D, Bet_4 A C D B /\ Cong A C C D /\ Cong C D D B). apply SegmTrisectExistence. destruct H as [D[C]]. spliter. exists C. split. unfold Bet_4 in H. spliter. apply H3. intros. assert(Midpoint D A C). unfold Midpoint. split. unfold Bet_4 in H. spliter. apply H. apply H0. assert(M = D). apply l7_17 with A C; finish. subst. CongR. Qed.
imports: sesamath_exercises