proposition: Lemma collect_wds_for_concy : forall A B C pa pb pc st interp, ~ Col A B C -> interp pa = A -> interp pb = B -> interp pc = C -> st_ok_for_concy st interp -> st_ok_for_concy (STadd (pa, (pb, pc)) st) interp.
proof: Proof. intros A B C pa pb pc st interp HNCol HA HB HC HST. apply (@collect_wds 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; 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