a:{...0}, n:{...-1}. (a 
n) 
a:{...0}, b:{...-1}. (a b) = ((-a) (-b))a:, n:
. (a n) | Rank | Theorem | Name |
| 4 | a:{...0}, n:{...-1}. (a n) | [division_typing2a_sfa] |
| cites the following: | ||
| 3 | a:{...0}, b:{...-1}. (a b) = ((-a) (-b)) | [div_3_to_1] |
| 3 | a:, n:. (a n) | [division_typing1a_sfa] |