proposition: Lemma conga_os__concyclic : forall A B C D, OS A B C D -> CongA A C B A D B -> Concyclic A B C D.
proof: Proof. intros A B C D HOS HConga. split. apply os__coplanar, HOS. destruct (triangle_circumscription A B C) as [O]; spliter. apply one_side_not_col123 with D, HOS. assert (OnCircle A O A /\ OnCircle B O A /\ OnCircle C O A). unfold OnCircle; repeat split; Cong. spliter. exists O, A; repeat split; trivial. apply (conga_cop_onc3_os__onc A B C); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec