x,y:
. x
y = 1 
x = 1 & y = 1a,b:
. 
ab = 0 
a = 0 & b = 0a,b:, n:
. na
nb ab| Rank | Theorem | Name |
| 3 | x,y:. xy = 1 x = 1 & y = 1 | [nat_prod_one_iff_factors_one] |
| cites the following: | ||
| 0 | a,b:. ab = 0 a = 0 & b = 0 | [zero_ann_b] |
| 2 | a,b:, n:. nanb ab | [mul_cancel_in_le] |