[STATEMENT]
lemma UP_SA_n_is_cring:
  shows "cring (UP (SA n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (UP (SA n))
[PROOF STEP]
using SA_is_cring
[PROOF STATE]
proof (prove)
using this:
cring (SA ?n)

goal (1 subgoal):
 1. cring (UP (SA n))
[PROOF STEP]
by (simp add: UP_cring.UP_cring UP_cring.intro)