proposition: Lemma bet_inc2__incs : forall O P U V X, X <> U -> X <> V -> Bet U X V -> InCircle U O P -> InCircle V O P -> InCircleS X O P.
proof: Proof. intros O P U V X HUX HVX HBet HUIn HVIn. destruct (le_cases O U O V). - apply le3456_lt__lt with O V; trivial. apply lt_comm, (bet_le__lt U); Le. - apply le3456_lt__lt with O U; trivial. apply lt_comm, (bet_le__lt V); Between; Le. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel