proposition: Lemma col_inc2_outcs__out : forall A B U V P, InCircle U A B -> InCircle V A B -> Col U V P -> OutCircleS P A B -> Out P U V.
proof: Proof. intros A B U V P HUIn HVIn HCol HOut. apply not_bet_out; Col. intro HBet. apply outcs__ninc in HOut. apply HOut, bet_inc2__inc with U V; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel