proposition: Lemma diam_uniqueness : forall O P A B X, Diam A B O P -> Cong A X A B -> OnCircle X O P -> X = B.
proof: Proof. intros. unfold Diam in *. spliter. unfold OnCircle in *. induction(eq_dec_points O P). treat_equalities; auto. assert(Bet A O X). { apply(l4_6 A O B A O X); auto. repeat split; Cong. apply cong_transitivity with O P; Cong. } assert_diffs. apply(between_cong_3 A O); auto. apply cong_transitivity with O P; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel