[STATEMENT]
lemma less_is_non_zero_p1:
  fixes a :: "'a :: len word"
  shows "a < k \<Longrightarrow> a + 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < k \<Longrightarrow> a + 1 \<noteq> 0
[PROOF STEP]
apply (erule contrapos_pn)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + 1 = 0 \<Longrightarrow> \<not> a < k
[PROOF STEP]
apply (drule max_word_wrap)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = - 1 \<Longrightarrow> \<not> a < k
[PROOF STEP]
apply (simp add: not_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done