int
2
Sections
StandardLIB
Doc
Rank
Theorem
Name
2
Thm*
a,b,n:
. a
b
a+n
b+n
[add_mono_wrt_le]
cites
1
Thm*
a,b,n:
. a+n
b+n
a
b
[add_cancel_in_le]
int
2
Sections
StandardLIB
Doc
a,b,n:
. a
b 
a+nb+na,b,n:. a+nb+n 
aba,b,n:. ab a+nb+na,b,n:. a+nb+n ab