[STATEMENT]
lemma (in linorder) sorted_wrt_rev_linord [simp] :
  "sorted_wrt (\<ge>) l \<longleftrightarrow> sorted (rev l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (\<lambda>x y. y \<le> x) l = sorted (rev l)
[PROOF STEP]
by (simp add: sorted_wrt_rev)