\begin{isabelle}% \isacommand{lemma}~{"}min~i~(max~j~(k*k))~=~max~(min~(k*k)~i)~(min~i~(j::nat)){"}\isanewline \isacommand{apply}(arith)\isacommand{.}\isanewline \end{isabelle}%