doc-src/TutorialI/Misc/document/AdvancedInd.tex

 \noindent
 If you find the last step puzzling, here are the two lemmas it employs:
 \begin{isabelle}
 \isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
 \rulename{Suc_leI}\isanewline
-\isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}
+\isa{{\isasymlbrakk}x\ {\isasymle}\ y{\isacharsemicolon}\ y\ {\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}\ z}
 \rulename{le_less_trans}
 \end{isabelle}
 %
 The proof goes like this (writing \isa{j} instead of \isa{nat}).
 Since \isa{i\ {\isacharequal}\ Suc\ j} it suffices to show