[STATEMENT]
lemma less_\<tau>D: "\<tau> \<sigma> i < \<tau> \<sigma> j \<Longrightarrow> i < j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<sigma> i < \<tau> \<sigma> j \<Longrightarrow> i < j
[PROOF STEP]
by (meson \<tau>_mono less_le_not_le not_le_imp_less)