Notation:

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

Top-level interaction 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)