[STATEMENT]
lemma two_step_less_D:
  "0 < two_step r \<Longrightarrow> two_step r = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < two_step r \<Longrightarrow> two_step r = Suc 0
[PROOF STEP]
by(auto simp add: two_step_def)