int
2
Sections
StandardLIB
Doc
Theorem
Name
Thm*
a,b,n:
. a = b
a+n = b+n
[add_mono_wrt_eq]
cites
Thm*
a,b,n:
. a+n = b+n
a = b
[add_cancel_in_eq]
int
2
Sections
StandardLIB
Doc
a,b,n:
. a = b 
a+n = b+na,b,n:. a+n = b+n 
a = ba,b,n:. a = b a+n = b+na,b,n:. a+n = b+n a = b