[STATEMENT]
lemma sorted2: "sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))
[PROOF STEP]
by(induction zs) auto