proposition: Lemma onc2_out__outcs : forall A B U V P, U <> V -> OnCircle U A B -> OnCircle V A B -> Out P U V -> OutCircleS P A B.
proof: Proof. intros A B U V P HUV HUOn HVOn HOut. apply outcs__ninc. intro HIn. apply (not_bet_and_out U P V). split; trivial. apply (col_inc_onc2__bet A B); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel