a,b:
, n:
. ((n
a) ~ (nb)) 
(a ~ b)a,b:. (a ~ b) 
a = b 
a = -ba,b:, n:. na = nb a = b| Rank | Theorem | Name |
| 6 | a,b:, n:. ((na) ~ (nb)) (a ~ b) | [mul_cancel_in_assoced] |
| cites the following: | ||
| 5 | a,b:. (a ~ b) a = b a = -b | [assoced_elim] |
| 3 | a,b:, n:. na = nb a = b | [mul_cancel_in_eq] |