proposition: Lemma collect_coincs_for_concy : forall A B C D pa pb pc pd ss interp, Concyclic_gen A B C D -> interp pa = A -> interp pb = B -> interp pc = C -> interp pd = D -> ss_ok_for_concy ss interp -> ss_ok_for_concy (SS.add (@CPToSS 4 (pa, (pb, (pc, pd)))) ss) interp.
proof: Proof. intros A B C D pa pb pc pd ss interp HConcy HA HB HC HD HSS. apply (@collect_coincs Tarski_is_a_Arity_for_concy Tarski_is_a_Coinc_predicates_for_concy); [apply Tarski_is_a_Coinc_theory_for_concy|simpl|auto]. rewrite HA; rewrite HB; rewrite HC; rewrite HD; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane NArith GeoCoq.Utils.sets GeoCoq.Meta_theory.Models.tarski_to_coinc_theory_for_concyclic GeoCoq.Tactics.Coinc.CoincR