a,b:
, n:
. a < b 
n
a < nbi,j:. i < j 
i+1
ji1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2| Rank | Theorem | Name |
| 2 |
Thm* a,b:, n:. a < b na < nb | [mul_preserves_lt] |
| cites | ||
| 1 |
Thm* i,j:. i < j i+1j | [lt_to_le_rw] |
| 0 |
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2 | [add_functionality_wrt_le] |