nat.bend checks

Zero is a right identity for addition: x + 0 = x.

Zero is a left identity for addition: 0 + x = x.

Adding a successor on the right: n + (m + 1) = (n + m) + 1.

Adding a successor on the left: (n + 1) + m = (n + m) + 1.

Addition is commutative: n + m = m + n.

Addition is associative: (a + b) + c = a + (b + c).

Left commutativity of addition: a + (b + c) = b + (a + c).

Right commutativity of addition: (a + b) + c = (a + c) + b.

Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d).

The successor function is injective: a + 1 = b + 1 implies a = b.

Zero is not a successor.

A successor is not zero.

Addition cancels on the left: a + b = a + c implies b = c.

Addition cancels on the right: a + b = c + b implies a = c.

Zero absorbs multiplication on the right: x * 0 = 0.

Zero absorbs multiplication on the left: 0 * x = 0.

One is a right identity for multiplication: x * 1 = x.

One is a left identity for multiplication: 1 * x = x.

Multiplying by a successor on the right: n * (m + 1) = n * m + n.

Multiplying by a successor on the left: (n + 1) * m = n * m + m.

Multiplication is commutative: n * m = m * n.

Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c.

Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c.

Multiplication is associative: (a * b) * c = a * (b * c).

Every natural is at most itself: a <= a.

Zero is at most every natural: 0 <= b.

Every natural is at most its successor: n <= n + 1.

Adding on the right never decreases a natural: n <= n + k.

The order is transitive: a <= b and b <= c imply a <= c.

The order is antisymmetric: a <= b and b <= a imply a = b.

The order is total: a <= b or b <= a.

The order is total, as a reusable sum: a <= b or b <= a.

No natural is less than itself.

The strict order is transitive: a < b and b < c imply a < c.

A strict inequality implies the weak one: a < b implies a <= b.

Flipping a >= b gives b <= a.

Flipping b <= a gives a >= b.

Flipping a > b gives b < a.

Flipping b < a gives a > b.

Zero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.

Zero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.

Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.

Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.

Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.

Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.

Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.

Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.

Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.

Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.

Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.

One is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.

One is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.

Multiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.

Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.

Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.

Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.

Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.

Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.

The order a <= b on naturals, as a reusable proposition.

The strict order a < b on naturals, as a reusable proposition.

The order a >= b on naturals, as a reusable proposition.

The strict order a > b on naturals, as a reusable proposition.