1
(*<*)
2
theory arith1 = Main:;
3
(*>*)
4
lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n";
5
(**)(*<*)
6
by(auto);
7
end
8