proposition: Lemma ss_ok_empty_for_concy : forall interp, ss_ok_for_concy SS.empty interp.
proof: Proof. exact ss_ok_empty. 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