[STATEMENT]
lemma zless_zle_trans:"\<lbrakk> (i::int) < j; j \<le> k\<rbrakk> \<Longrightarrow> i < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < j; j \<le> k\<rbrakk> \<Longrightarrow> i < k
[PROOF STEP]
by arith