int
2
Sections
StandardLIB
Doc
Rank
Theorem
Name
3
Thm*
a,b:
, n:
. n
a = n
b
a = b
[mul_cancel_in_eq]
cites
2
Thm*
a,b:
, n:
. a < b
n
a < n
b
[mul_preserves_lt]
int
2
Sections
StandardLIB
Doc
a,b:
, n:
. n
a = nb 
a = ba,b:, n:
. a < b na < nba,b:, n:. na = nb a = ba,b:, n:. a < b na < nb