proposition: Lemma onc3_ts__obtuse : forall O P A B C, OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> TS A B O C -> Obtuse A C B.
proof: Proof. intros O P A B C HA HB HC HTS. destruct (chord_completion O P C O) as [C' []]; Circle. assert (TS A B C C') by (apply bet_ts__ts with O; Side). apply (acute_suppa__obtuse A C' B). apply (onc3_os__acute O P); trivial; exists C; split; Side. apply (diam_onc2_ts__suppa O P); Side. repeat split; Between. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec