proposition: Lemma inc__radius : forall O P X, InCircle X O P -> exists Y, OnCircle Y O P /\ Bet O X Y.
proof: Proof. intros O P X HIn. destruct (eq_dec_points O P). unfold InCircle in HIn; treat_equalities. exists O; split; Circle; Between. destruct (eq_dec_points O X). subst; exists P; split; Circle; Between. destruct (segment_construction_3 O X O P) as [Y [HY1 HY2]]; auto. exists Y; split; auto. apply l6_13_1; trivial. apply (l5_6 O X O P); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel