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.

Subtracting zero changes nothing: n - 0 = n.

Truncated subtraction from zero is zero: 0 - n = 0.

A natural minus itself is zero: n - n = 0.

Subtracting successors: (n + 1) - (m + 1) = n - m.

Adding then subtracting m cancels: (n + m) - m = n.

Adding then subtracting n cancels: (n + m) - n = m.

If m <= n, subtracting and adding m back gives n: (n - m) + m = n.

Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k).

Truncated subtraction never increases: n - m <= n.

Minimum is commutative.

Maximum is commutative.

The minimum of a natural and itself is itself.

The maximum of a natural and itself is itself.

The minimum with zero is zero: min(a, 0) = 0.

The minimum with zero is zero: min(0, a) = 0.

Zero is an identity for maximum: max(a, 0) = a.

Zero is an identity for maximum: max(0, a) = a.

Minimum is associative.

Maximum is associative.

The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b.

The minimum is at most its left argument.

The minimum is at most its right argument.

The left argument is at most the maximum.

The right argument is at most the maximum.

Any natural to the power zero is one.

A power with a successor exponent: a^(n+1) = a * a^n.

Any natural to the power one is itself.

One to any power is one.

Exponents add under multiplication: a^(m+n) = a^m * a^n.

Doubling is adding a natural to itself.

Every natural tests equal to itself.

The equality test is symmetric.

If the equality test says true, the naturals are equal.

A >= b tests the same as b <= a.

A > b tests the same as b < a.

A < b tests the same as a + 1 <= b.

Not (a <= b) tests the same as b < a.

Not (a < b) tests the same as b <= a.

Every natural is less than its successor: n < n + 1.

The successor preserves the order: a <= b implies a + 1 <= b + 1.

The order of successors is the order of the naturals: a + 1 <= b + 1 implies a <= b.

A < b and b <= c imply a < c.

A <= b and b < c imply a < c.

Adding on the left preserves the order: a <= b implies k + a <= k + b.

The only natural at most zero is zero.

No natural is less than zero.

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.

Subtracting zero changes nothing: n - 0 = n, reversed to rewrite toward the simple side.

Truncated subtraction from zero is zero: 0 - n = 0, reversed to rewrite toward the simple side.

A natural minus itself is zero: n - n = 0, reversed to rewrite toward the simple side.

Subtracting successors: (n + 1) - (m + 1) = n - m, reversed to rewrite toward the simple side.

Adding then subtracting m cancels: (n + m) - m = n, reversed to rewrite toward the simple side.

Adding then subtracting n cancels: (n + m) - n = m, reversed to rewrite toward the simple side.

Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k), reversed to rewrite toward the simple side.

Minimum is commutative, reversed to rewrite toward the simple side.

Maximum is commutative, reversed to rewrite toward the simple side.

The minimum of a natural and itself is itself, reversed to rewrite toward the simple side.

The maximum of a natural and itself is itself, reversed to rewrite toward the simple side.

The minimum with zero is zero: min(a, 0) = 0, reversed to rewrite toward the simple side.

The minimum with zero is zero: min(0, a) = 0, reversed to rewrite toward the simple side.

Zero is an identity for maximum: max(a, 0) = a, reversed to rewrite toward the simple side.

Zero is an identity for maximum: max(0, a) = a, reversed to rewrite toward the simple side.

Minimum is associative, reversed to rewrite toward the simple side.

Maximum is associative, reversed to rewrite toward the simple side.

The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b, reversed to rewrite toward the simple side.

Any natural to the power zero is one, reversed to rewrite toward the simple side.

A power with a successor exponent: a^(n+1) = a * a^n, reversed to rewrite toward the simple side.

Any natural to the power one is itself, reversed to rewrite toward the simple side.

One to any power is one, reversed to rewrite toward the simple side.

Exponents add under multiplication: a^(m+n) = a^m * a^n, reversed to rewrite toward the simple side.

Doubling is adding a natural to itself, reversed to rewrite toward the simple side.

Every natural tests equal to itself, reversed to rewrite toward the simple side.

The equality test is symmetric, reversed to rewrite toward the simple side.

A >= b tests the same as b <= a, reversed to rewrite toward the simple side.

A > b tests the same as b < a, reversed to rewrite toward the simple side.

A < b tests the same as a + 1 <= b, reversed to rewrite toward the simple side.

Not (a <= b) tests the same as b < a, reversed to rewrite toward the simple side.

Not (a < b) tests the same as b <= a, 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.