proposition: Lemma bet_incs2__incs : forall O P U V X, Bet U X V -> InCircleS U O P -> InCircleS V O P -> InCircleS X O P.
proof: Proof. intros O P U V X HBet HUIn HVIn. destruct (eq_dec_points X U). subst; assumption. destruct (eq_dec_points X V). subst; assumption. apply bet_inc2__incs with U V; Circle. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel