proposition: Lemma cop_onc4_ts__suppa : forall O P A B C C', OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle C' O P -> TS A B C C' -> Coplanar A B C O -> SuppA A C B A C' B.
proof: Proof. intros O P A B C C' HA HB. revert C C'. assert (Haux : forall C C', OnCircle C O P -> OnCircle C' O P -> TS A B C C' -> OS A B O C -> SuppA A C B A C' B). { intros C C' HC HC' HTS HOS. suma.assert_diffs. assert (~ Col C A B) by (destruct HTS; assumption). assert (Coplanar A B C' O) by (apply coplanar_trans_1 with C; Cop). destruct (cop2_onc4__or_conga_suppa O P A B C C') as [Habs|]; Cop. exfalso. assert (HLta : LtA A C B A C' B); [|destruct HLta as [_ HN]; apply HN, Habs]. apply acute_obtuse__lta. apply (onc3_os__acute O P); assumption. apply (onc3_ts__obtuse O P); trivial. apply l9_8_2 with C; Side. } intros C C' HC HC' HTS HCop. assert (~ Col C A B) by (destruct HTS; assumption). destruct (col_dec A B O). { suma.assert_diffs. assert (Midpoint O A B) by (apply col_onc2__mid with P; auto). destruct HTS as [_ []]. apply per2__suppa; auto; apply thales_theorem with O; trivial; apply onc2__cong with P; assumption. } destruct (cop__one_or_two_sides A B O C); Col; Cop. apply suppa_sym, Haux; [..|exists C; split]; Side. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec