proposition: Lemma bet_cop_onc2__ex_onc_os_out : forall O P A B C I, A <> I -> B <> I -> ~ Col A B C -> ~ Col A B O -> OnCircle A O P -> OnCircle B O P -> Bet A I B -> Coplanar A B C O -> exists C1, Out C1 O I /\ OnCircle C1 O P /\ OS A B C C1.
proof: Proof. intros O P A B C I HAI HBI HNCol HNCol1 HA HB HBet HCop. destruct (diam_points O P I) as [C1 [C2 [HBet1 [HCol [HC1 HC2]]]]]. assert (HTS : TS A B C1 C2). { apply (chord_intersection O P); trivial. unfold OnCircle in *; assert_diffs. repeat split; [intro; apply HNCol1; ColR..|exists I; split; Col]. } assert (HBet2 : Bet C1 I C2). { assert_diffs; apply (col_inc_onc2__bet O P); auto. apply bet_inc2__inc with A B; Circle. } assert (HNCol2 : ~ Col C1 A B) by (destruct HTS; assumption). destruct (cop__one_or_two_sides A B C C1); Col. apply coplanar_trans_1 with O; Col; [Cop|exists I; right; right; assert_diffs; split; ColR]. - exists C2. split; [|split; trivial; exists C1; Side]. apply bet2__out with C1; Between. intro; treat_equalities; auto. destruct HTS as [_ [HNCol3 _]]; spliter; intro; subst; apply HNCol3; Col. - exists C1. split; [|split; trivial]. apply bet2__out with C2; trivial. intro; treat_equalities; auto. intro; subst; apply HNCol2; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel