[STATEMENT]
lemma length_nonempty: 
assumes "x \<noteq> []" 
shows    "Suc 0 \<le> length x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc 0 \<le> length x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> []

goal (1 subgoal):
 1. Suc 0 \<le> length x
[PROOF STEP]
by (metis length_greater_0_conv less_eq_Suc_le)