1
(*<*)
2
theory arith2 = Main:;
3
(*>*)
4
lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
5
apply(arith).;
6
(**)(*<*)
7
end
8