proposition: Lemma cop_obtuse_onc3__ts : forall O P A B C, OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O -> Obtuse A C B -> TS A B O C.
proof: Proof. intros O P A B C HA HB HC HCop HObtuse. suma.assert_diffs. assert (~ Col A B C) by (apply (onc3__ncol O P); auto). apply coplanar_perm_1 in HCop. apply cop_nos__ts; Col; intro Habs; apply (nlta A C B). - apply obtuse_per__lta; auto. apply thales_theorem with O; trivial. apply col_onc2__mid with P; Col. apply (onc2__cong O P); assumption. - apply acute_obtuse__lta; trivial. apply (onc3_os__acute O P); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec