proposition: Lemma cop_onc4_os__conga : forall O P A B C C', OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle C' O P -> OS A B C C' -> Coplanar A B C O -> CongA A C B A C' B.
proof: Proof. intros O P A B C C' HA HB HC HC' HOS HCop. assert_ncols. destruct (col_dec A B O). { suma.assert_diffs. assert (Midpoint O A B) by (apply col_onc2__mid with P; auto). apply l11_16; auto; apply thales_theorem with O; Col; apply cong_transitivity with O P; Cong. } destruct (cop__one_or_two_sides A B O C); Col; Cop. - suma.assert_diffs; destruct (cop2_onc4__or_conga_suppa O P A B C C') as [|Habs]; auto. apply coplanar_trans_1 with C; Col; Cop. exfalso. apply (nlta A C' B), acute_obtuse__lta. apply (obtuse_suppa__acute A C B); [apply (onc3_ts__obtuse O P)|]; trivial. apply (onc3_ts__obtuse O P); trivial; apply l9_2, l9_8_2 with C; Side. - apply ghalfa2__conga_2 with A O B; apply inscribed_angle with P; trivial. apply one_side_transitivity with C; Side. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec