[STATEMENT]
lemma ac_cong_set2_is_semialg:
  assumes "k \<in> Units (Zp_res_ring n)"
  assumes "n > 0"
  shows "is_semialgebraic 2 (ac_cong_set2 n k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_semialgebraic 2 (ac_cong_set2 n k)
[PROOF STEP]
using  ac_cong_set_is_univ_semialg ac_cong_set2_cartesian_product[of k n]
      cartesian_product_is_semialgebraic[of 1 "((\<lambda>a. [a]) ` ac_cong_set n k)" 1 " ((\<lambda>a. [a]) ` val_ring_constant_ac_set n k)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?n; ?k \<in> Units (residue_ring (p ^ ?n))\<rbrakk> \<Longrightarrow> is_univ_semialgebraic (ac_cong_set ?n ?k)
\<lbrakk>k \<in> Units (residue_ring (p ^ n)); 0 < n\<rbrakk> \<Longrightarrow> ac_cong_set2 n k = cartesian_product ((\<lambda>a. [a]) ` ac_cong_set n k) ((\<lambda>a. [a]) ` val_ring_constant_ac_set n k)
\<lbrakk>is_semialgebraic 1 ((\<lambda>a. [a]) ` ac_cong_set n k); is_semialgebraic 1 ((\<lambda>a. [a]) ` val_ring_constant_ac_set n k)\<rbrakk> \<Longrightarrow> is_semialgebraic (1 + 1) (cartesian_product ((\<lambda>a. [a]) ` ac_cong_set n k) ((\<lambda>a. [a]) ` val_ring_constant_ac_set n k))

goal (1 subgoal):
 1. is_semialgebraic 2 (ac_cong_set2 n k)
[PROOF STEP]
by (metis assms(1) assms(2) is_univ_semialgebraicE less_one less_or_eq_imp_le nat_neq_iff
      one_add_one val_ring_constant_ac_set_is_univ_semialgebraic zero_not_in_residue_units)