PrintForm
Definitions
Lemmas
hol
arithmetic
3
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
less
mono
rev
m
,
n
:
.
m
+1<
n
+1
m
<
n
By:
RewriteOfThm Thm* all(
m
:hnum. all(
n
:hnum. implies(lt(suc(
m
),suc(
n
)),lt(
m
,
n
))))
(SimpsetC [`hol_to_nuprl`;`bequal`])
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
arithmetic
3
Sections
HOLlib
Doc