proposition: Lemma inc_onc2_out__eq : forall O P A B C, InCircle A O P -> OnCircle B O P -> OnCircle C O P -> Out A B C -> B = C.
proof: Proof. intros O P A B C HA HB HC HOut. destruct (chord_completion O P B A) as [B' [HB' HBet]]; trivial. assert_diffs. destruct (line_circle_two_points O P B B' C); auto. ColR. subst C. exfalso. apply (not_bet_and_out B A B'); split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel