equal
deleted
inserted
replaced
28 of your function once more. In our case the required lemma is the obvious one:% |
28 of your function once more. In our case the required lemma is the obvious one:% |
29 \end{isamarkuptext}% |
29 \end{isamarkuptext}% |
30 \isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}% |
30 \isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}% |
31 \begin{isamarkuptxt}% |
31 \begin{isamarkuptxt}% |
32 \noindent |
32 \noindent |
33 It was not proved automatically because of the special nature of \isa{{\isacharminus}} |
33 It was not proved automatically because of the special nature of subtraction |
34 on \isa{nat}. This requires more arithmetic than is tried by default:% |
34 on \isa{nat}. This requires more arithmetic than is tried by default:% |
35 \end{isamarkuptxt}% |
35 \end{isamarkuptxt}% |
36 \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline |
36 \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline |
37 \isacommand{done}% |
37 \isacommand{done}% |
38 \begin{isamarkuptext}% |
38 \begin{isamarkuptext}% |