[STATEMENT]
lemma less_eq_list_code [code]:
  "x # xs \<le> ([]::'a::{equal, order} list) \<longleftrightarrow> False"
  "[] \<le> (xs::'a::{equal, order} list) \<longleftrightarrow> True"
  "(x::'a::{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs \<le> []) = False &&& ([] \<le> xs) = True &&& (x # xs \<le> y # ys) = (x < y \<or> x = y \<and> xs \<le> ys)
[PROOF STEP]
by simp_all