[STATEMENT]
lemma hd_sort:
  fixes xs :: "'a :: linorder list"
  shows "xs \<noteq> [] \<Longrightarrow> hd (sort xs) = Min (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> hd (sort xs) = Min (set xs)
[PROOF STEP]
by (subst Min_set_sorted [symmetric]) auto