(15steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
divide
wf
1
2
1
1.
a:
2.
n:
0 < (a
n)+1
By:
Using [`n',n] (BackThru
Thm*
a,b:
, n:
. n
a < n
b
a < b)
Generated subgoal:
1
n
0 < n
((a
n)+1)
About:
(15steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
n
0 < n((a 
n)+1)
0 < (a n)+1
a,b:
, n:. na < nb 
a < b) n0 < n((a n)+1)
