x,y,z:
. x =q y 
y =q z x =q zx,y:
. x=
y 
x = yi1,i2,j1,j2:. i1 = j1 i2 = j2 i1
i2 = j1j2a,b:. ab = 0 a = 0 
b = 0a,b:, n:
. na = nb a = ba,b:. a 
0 b 0 ab 0| Rank | Theorem | Name |
| 5 | x,y,z:. x =q y y =q z x =q z | [eq_rat_trans] |
| cites the following: | ||
| 1 | x,y:. x=y x = y | [assert_of_eq_int_rw] |
| 0 | i1,i2,j1,j2:. i1 = j1 i2 = j2 i1i2 = j1j2 | [mul_functionality_wrt_eq] |
| 4 | a,b:. ab = 0 a = 0 b = 0 | [int_entire] |
| 3 | a,b:, n:. na = nb a = b | [mul_cancel_in_eq] |
| 4 | a,b:. a 0 b 0 ab 0 | [int_entire_a] |