proposition: Lemma SegmTrisectFirstThirdUniqueness: forall A B C D, FirstThird C A B -> FirstThird D A B -> C = D.
proof: Proof. intros. unfold FirstThird in *. spliter. Name S the second_third of A and B. assert(Midpoint C A S);auto. assert(Midpoint D A S);auto. apply l7_17 with A S;auto. Qed.
imports: sesamath_exercises