[STATEMENT]
lemma hadd_succ_right [simp]: "x @+ succ y = succ (x @+ y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x @+ succ y = succ (x @+ y)
[PROOF STEP]
by (metis hadd_hinsert_right succ_def)