proposition: Lemma conga_cop_onc3_os__onc : forall A B C D O P, OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O -> OS A B C D -> CongA A C B A D B -> OnCircle D O P.
proof: Proof. intros A B C D O P HA HB HC HCop HOS HConga. destruct (triangle_circumscription A B D) as [O']. apply one_side_not_col124 in HOS; Col. spliter. assert (OnCircle A O' A /\ OnCircle B O' A /\ OnCircle D O' A). unfold OnCircle; repeat split; Cong. spliter. apply (conga_cop_onc6_os__eqc A B C D O P O' A); trivial. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec