(4steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
div
unique
1
1
1
1.
n:
2.
p:
3.
q:
4.
n
p < n
(q+1)
5.
n
q < n
(p+1)
p = q
By:
FwdThru
Thm*
a,b:
, n:
. n
a < n
b
a < b [4]
THEN
FwdThru
Thm*
a,b:
, n:
. n
a < n
b
a < b [5]
Generated subgoals:
None
About:
(4steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
p < n(q+1)q < n(p+1)
p = q
a,b:
, n:. na < nb 
a < b
[4]
a,b:, n:. na < nb a < b
[5]