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