proposition: Lemma SegmTrisectFirstThirdExistence: forall A B, exists F,FirstThird F 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 [C[D]]. spliter. exists C. split. unfold Bet_4 in H. spliter. apply H4. intros. unfold SecondThird in H2;spliter. Name M the midpoint of A and S. assert(Cong A M S B);auto. assert(Cong A M M S);finish. assert(Cong M S S B). CongR. assert(C = M /\ D = S). { assert(Bet_4 A C D B);auto. assert(Cong A C C D);auto. assert(Cong C D D B);auto. assert(Bet_4 A M S B). { split;finish. split. assert(Bet A M S);finish. apply between_exchange3 with A;auto. split. auto. apply between_exchange4 with S;auto. finish. } assert(Cong A M M S);auto. assert(Cong M S S B);auto. apply SegmTrisectUniqueness with A B. split;auto. } spliter. subst. auto. Qed.
imports: sesamath_exercises