proposition: Lemma bet_inc2__inc : forall A B U V P, InCircle U A B -> InCircle V A B -> Bet U P V -> InCircle P A B.
proof: Proof. intros A B U V P HU HV HBet. destruct (eq_dec_points P U). subst P; assumption. destruct (eq_dec_points P V). subst P; assumption. apply incs__inc, bet_inc2__incs with U V; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel