proposition: Lemma conga_cop2_onc4__os : 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 -> CongA A C B A D B -> OS A B C D.
proof: Proof. intros O P A B C D HNCol HA HB HC HD HCopC HCopD HConga. suma.assert_diffs. destruct (angle_partition A C B) as [HAcute|[HPer|HObtuse]]; auto. - apply one_side_transitivity with O; [apply one_side_symmetry|]; apply acute_cop_onc3__os with P; Cop. apply (acute_conga__acute A C B); assumption. - exfalso. apply HNCol, col_permutation_1, midpoint_col. assert (HCong := onc2__cong O P). apply thales_converse_theorem_1 with C; Cop. - exists O; split; apply l9_2; apply cop_obtuse_onc3__ts with P; Cop. apply (conga_obtuse__obtuse A C B); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec