int
2
Sections
StandardLIB
Doc
Rank
Theorem
Name
2
Thm*
a,b:
, n:
. n
a < n
b
a < b
[mul_cancel_in_lt]
cites
1
Thm*
a,b:
, n:
. a
b
n
a
n
b
[mul_preserves_le]
int
2
Sections
StandardLIB
Doc
a,b:
, n:
. n
a < nb 
a < ba,b:, n:. a
b nanba,b:, n:. na < nb a < ba,b:, n:. ab nanb