Notation:

m,n,k:  natural numbers
a,b,c:  types of kind Nat

Top-level interactions for TypeNat:

TypeNat m

Top-level interactions for <=

m <= n   <=> {m <= n} = True
0 <= a   <=> True
a <= 0   <=> a ~ 0

Top-level interactions for +.

(m + n ~ k) <=> {m + n} = k
(m + a ~ n) <=> a ~ {n - m}    -- n >= m
(a + m ~ n) <=> a ~ {n - m}    -- n >= m
(0 + a ~ b) <=> a ~ b
(a + 0 ~ b) <=> a ~ b
(a + b ~ 0) <=> (a ~ 0, b ~ 0)
(a + b ~ a) <=> (b ~ 0)
(a + b ~ b) <=> (a ~ 0)
(a + a ~ b) <=> (2 * a ~ b)

Top-level interactions for *.

(m * n ~ k) <=> {m * n} = k
(m * a ~ n) <=> a ~ {n / m}     -- m `divides` n
(a * m ~ n) <=> a ~ {n / m}     -- m `divides` n
(0 * a ~ b) <=> b ~ 0
(a * 0 ~ b) <=> b ~ 0
(1 * a ~ b) <=> a ~ b
(a * 1 ~ b) <=> a ~ b
(a * b ~ 1) <=> (a ~ 1, b ~ 1)
(a + a ~ b) <=> 2 ^ a ~ b

Top-level interactions for ^

(m ^ n ~ k) <=> {m ^ n} = k
(m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists
(a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists
(a ^ 0 ~ b) <=> b ~ 1
(1 ^ a ~ b) <=> b ~ 1