[STATEMENT]
lemma sup_less_eq_cases_3:
  "-y \<squnion> -x \<le> -z \<squnion> -x \<Longrightarrow> -y \<squnion> --x \<le> -z \<squnion> --x \<Longrightarrow> -y \<le> -z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- y \<squnion> - x \<le> - z \<squnion> - x; - y \<squnion> - - x \<le> - z \<squnion> - - x\<rbrakk> \<Longrightarrow> - y \<le> - z
[PROOF STEP]
by (simp add: sup_less_eq_cases_2 sub_commutative)