proposition: Lemma test_coinc_ok_for_cop : forall pa pb pc pd ss st interp, ss_ok_for_cop ss interp -> st_ok_for_cop st interp -> test_coinc_for_cop ss st pa pb pc pd = true -> Coplanar (interp pa) (interp pb) (interp pc) (interp pd).
proof: Proof. intros pa pb pc pd ss st interp HSS HST HTest. assert (HCop := @test_coinc_ok Tarski_is_a_Arity_for_cop Tarski_is_a_Coinc_predicates_for_cop Tarski_is_a_Coinc_theory_for_cop ss st interp (pa, (pb, (pc, pd))) HSS HST HTest). simpl in HCop; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane NArith GeoCoq.Utils.sets GeoCoq.Meta_theory.Models.tarski_to_coinc_theory_for_cop GeoCoq.Tactics.Coinc.CoincR