proposition: Lemma diam_points : forall O P X, exists Q1 Q2, Bet Q1 O Q2 /\ Col Q1 Q2 X /\ OnCircle Q1 O P /\ OnCircle Q2 O P.
proof: Proof. intros O P X. destruct (eq_dec_points X O). subst X. destruct (segment_construction P O O P) as [P' [HP'1 HP'2]]. exists P, P'; repeat split; Col; Circle. destruct (eq_dec_points O P). subst P. exists O, O; repeat split; finish. assert(HH:= onc_exists O P X H H0). ex_and HH Q1. assert(HH:= segment_construction Q1 O O Q1). ex_and HH Q2. exists Q1, Q2. repeat split; Col. ColR. apply cong_transitivity with O Q1; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel