[STATEMENT]
lemma word_less_minus_mono_left: "y < z \<Longrightarrow> x \<le> y \<Longrightarrow> y - x < z - x"
  for x y z :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < z; x \<le> y\<rbrakk> \<Longrightarrow> y - x < z - x
[PROOF STEP]
by uint_arith