i1,i2,j1,j2:
. i1
j1 
i2
j2 i1-i2j1-j2i,j:. ij -i-ji1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2| Rank | Theorem | Name |
| 2 |
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1-i2j1-j2 | [sub_functionality_wrt_le] |
| cites | ||
| 1 |
Thm* i,j:. ij -i-j | [minus_functionality_wrt_le] |
| 0 |
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2 | [add_functionality_wrt_le] |