proposition: Lemma cop2_onc4_suppa__ts : forall O P A B C D, ~ Col A B O -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle D O P -> Coplanar A B O C -> Coplanar A B O D -> SuppA A C B A D B -> TS A B C D.
proof: Proof. intros O P A B C D HNCol HA HB HC HD HCopC HCopD HSuppa. suma.assert_diffs. destruct (angle_partition A C B) as [HAcute|[HPer|HObtuse]]; auto. - apply l9_8_2 with O. apply cop_obtuse_onc3__ts with P; Cop; apply (acute_suppa__obtuse A C B); assumption. apply acute_cop_onc3__os with P; Cop. - exfalso. apply HNCol, col_permutation_1, midpoint_col. assert (HCong := onc2__cong O P). apply thales_converse_theorem_1 with C; Cop. - apply l9_2, l9_8_2 with O. apply cop_obtuse_onc3__ts with P; Cop. apply acute_cop_onc3__os with P; Cop; apply (obtuse_suppa__acute A C B); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec