proposition: Theorem SegmTrisectExistenceUniqueness: forall A B, exists! C D, Bet_4 A C D B /\ Cong A C C D /\ Cong C D D B.
proof: Proof. intros. assert(exists C, exists D, Bet_4 A C D B /\ Cong A C C D /\ Cong C D D B) by (apply SegmTrisectExistence). destruct H as [C [D]]. spliter. exists C. unfold unique. split. exists D. split. auto. intros. spliter. eapply SegmTrisectUniqueness. split. apply H. split. apply H0. split. apply H1. split. apply H2. split; finish. intros. destruct H2 as [E]. spliter. assert(C = x' /\ D = E). { eapply SegmTrisectUniqueness. split. apply H. split;finish. } tauto. Qed.
imports: sesamath_exercises