i1,i2,j1,j2:
. i1 < j1 
i2
j2 i1+i2 < j1+j2i,j:. i < j 
i+1ji1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2| Theorem | Name |
|
Thm* i1,i2,j1,j2:. i1 < j1 i2j2 i1+i2 < j1+j2 | [add_functionality_wrt_lt] |
| cites | |
| Thm* i,j:. i < j i+1j | [lt_to_le] |
|
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2 | [add_functionality_wrt_le] |