add_both_monus: (all z:Nat, y:Nat, x:Nat. (z + y) ∸ (z + x) = y ∸ x)

add_monus_identity: (all m:Nat. (all n:Nat. (m + n) ∸ m = n))

monus_monus_eq_monus_add: (all x:Nat. (all y:Nat. (all z:Nat. (x ∸ y) ∸ z = x ∸ (y + z))))

monus_order: (all x:Nat, y:Nat, z:Nat. (x ∸ y) ∸ z = (x ∸ z) ∸ y)