[STATEMENT]
lemma steps_Suc: "(x, y) \<in> steps rel (Suc n) \<longleftrightarrow>
  (x, y) \<in> steps rel n \<or> (x, n) \<in> steps rel n \<and> (n, y) \<in> steps rel n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> steps rel (Suc n)) = ((x, y) \<in> steps rel n \<or> (x, n) \<in> steps rel n \<and> (n, y) \<in> steps rel n)
[PROOF STEP]
by auto