proposition: Lemma col_inc_onc2__bet : forall A B U V P, U <> V -> OnCircle U A B -> OnCircle V A B -> Col U V P -> InCircle P A B -> Bet U P V.
proof: Proof. intros A B U V P HUV HU HV HCol HIn. destruct (eq_dec_points P U); [subst; Between|]. destruct (eq_dec_points P V); [subst; Between|]. assert (Cong A U A V) by (apply (onc2__cong A B); assumption). apply out2__bet; apply not_bet_out; Col; intro. - apply (bet_le__lt P V A U); Cong. apply (l5_6 A P A B); Cong. - apply (bet_le__lt P U A V); Between; Cong. apply (l5_6 A P A B); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel