proposition: Lemma acute_cop_onc3__os : forall O P A B C, A <> B -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O -> Acute A C B -> OS A B O C.
proof: Proof. intros O P A B C HAB HA HB HC HCop HAcute. suma.assert_diffs. assert (~ Col A B C) by (apply (onc3__ncol O P); auto). apply coplanar_perm_1 in HCop. apply cop_nts__os; Col; intro Habs; apply (nlta A C B). - apply acute_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_ts__obtuse O P); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec