x:
, y,z:. x = y
z 
(x 
z) = yx,y:, z:. x = yz (x z) = ya,b:. 0<ab 
0<a & 0<b| Rank | Theorem | Name |
| 5 | x:, y,z:. x = yz (x z) = y | [div_inverts_nat_mul2] |
| cites the following: | ||
| 3 | x,y:, z:. x = yz (x z) = y | [div_inverts_nat_mul] |
| 4 | a,b:. 0<ab 0<a & 0<b | [pos_mul_arg_boundsNat] |