proposition: Lemma prop_2 : forall O P U V X, X <> U -> X <> V -> Bet U X V -> OnCircle U O P -> OnCircle V O P -> InCircleS X O P.
proof: Proof. intros O P U V X; intros. apply bet_inc2__incs with U V; Circle. Qed.
imports: GeoCoq.Tarski_dev.Annexes.tangency GeoCoq.Tarski_dev.Annexes.inscribed_angle