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.

The division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a.

A number at most b divides by 1 + b to zero: a <= b implies a / (1 + b) = 0.

Division by a positive divisor is monotone: a <= c implies a / (1 + b) <= c / (1 + b).

Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b).

A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a.

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.

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

Adding the same amount on the left does not change the order test: a <= b tests as k + a <= k + b.

Adding two bounded summands stays bounded: a <= c and b <= d imply a + b <= c + d.

A sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both.

The only natural at most zero is zero.

No natural is less than zero.

A strict inequality rules out the reverse weak one: a < b implies b <= a is false.

A weak inequality rules out the reverse strict one: a <= b implies b < a is false.

A failed weak test gives the reverse strict order: a <= b false implies b < a.

A failed strict test gives the reverse weak order: a < b false implies b <= a.

A number below both bounds is below their minimum: a < b and a < c imply a < min b c.

The minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c.

The maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c.

Subtracting a larger number gives zero: a <= b implies a - b = 0.

Above the subtrahend, a successor subtracts to a successor: b <= a implies (a + 1) - b = (a - b) + 1.

Adding back what was subtracted restores the number: a <= b implies a + (b - a) = b.

Comparing against a difference is comparing the sum: a < c - b tests as b + a < c.

A witnessed difference gives the order: a + k = b implies a <= b.

Multiplying on the right preserves the order: a <= b implies a * k <= b * k.

Zero divided by anything is zero: 0 / b = 0.

Zero modulo anything is zero: 0 % b = 0.

Dividing by one changes nothing: a / 1 = a.

Any natural modulo one is zero: a % 1 = 0.

A natural modulo itself is zero: n % n = 0.

A positive natural divided by itself is one: (1 + b) / (1 + b) = 1.

A remainder is below its positive divisor: a % (1 + b) < 1 + b.

A remainder never exceeds the dividend: a % b <= a.

A quotient never exceeds the dividend: a / b <= a.

A number below the divisor is its own remainder: a < b implies a % b = a.

Taking a remainder twice is taking it once: (a % n) % n = a % n.

Adding the divisor does not change the remainder: (b + a) % b = a % b.

Multiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a.

Multiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a.

A multiple of b leaves no remainder modulo b: (a * b) % b = 0.

A multiple of a leaves no remainder modulo a: (a * b) % a = 0.

The remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a.

The quotient times the divisor never exceeds the dividend: (a / b) * b <= a.

Left commutativity of multiplication: a * (b * c) = b * (a * c).

Right commutativity of multiplication: (a * b) * c = (a * c) * b.

Four-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d).

Zero to a positive power is zero: 0^(n+1) = 0.

A power of a product is the product of the powers: (a * b)^n = a^n * b^n.

Exponents multiply under repeated powers: a^(m * n) = (a^m)^n.

A power of a positive base is at least one: 1 <= (1 + a)^n.

A power of a positive base is positive: 0 < (1 + a)^n.

Adding on the left never decreases a natural: n <= m + n.

A common left summand cancels in a difference: (k + n) - (k + m) = n - m.

A common right summand cancels in a difference: (n + k) - (m + k) = n - m.

Subtracting a part of the right summand: k <= m implies (n + m) - k = n + (m - k).

Subtracting a difference from its minuend: m <= n implies n - (n - m) = m.

Multiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k.

Multiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k.

The minimum is the smaller argument on the left: a <= b implies min a b = a.

The minimum is the smaller argument on the right: b <= a implies min a b = b.

The maximum is the larger argument on the left: b <= a implies max a b = a.

The maximum is the larger argument on the right: a <= b implies max a b = b.

A number is at most the minimum exactly when it is at most both: a <= min b c tests as a <= b and a <= c.

The maximum is at most c exactly when both arguments are: max a b <= c tests as a <= c and b <= c.

Multiplying on the left preserves the order: a <= b implies k * a <= k * b.

Multiplying two bounded factors stays bounded: a <= c and b <= d imply a * b <= c * d.

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.

The division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a, reversed to rewrite toward the simple side.

Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b), reversed to rewrite toward the simple side.

A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a, 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.

Adding the same amount on the left does not change the order test: a <= b tests as k + a <= k + b, reversed to rewrite toward the simple side.

A sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both, reversed to rewrite toward the simple side.

The minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c, reversed to rewrite toward the simple side.

The maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c, reversed to rewrite toward the simple side.

Comparing against a difference is comparing the sum: a < c - b tests as b + a < c, reversed to rewrite toward the simple side.

Zero divided by anything is zero: 0 / b = 0, reversed to rewrite toward the simple side.

Zero modulo anything is zero: 0 % b = 0, reversed to rewrite toward the simple side.

Dividing by one changes nothing: a / 1 = a, reversed to rewrite toward the simple side.

Any natural modulo one is zero: a % 1 = 0, reversed to rewrite toward the simple side.

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

A positive natural divided by itself is one: (1 + b) / (1 + b) = 1, reversed to rewrite toward the simple side.

Taking a remainder twice is taking it once: (a % n) % n = a % n, reversed to rewrite toward the simple side.

Adding the divisor does not change the remainder: (b + a) % b = a % b, reversed to rewrite toward the simple side.

Multiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a, reversed to rewrite toward the simple side.

Multiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a, reversed to rewrite toward the simple side.

A multiple of b leaves no remainder modulo b: (a * b) % b = 0, reversed to rewrite toward the simple side.

A multiple of a leaves no remainder modulo a: (a * b) % a = 0, reversed to rewrite toward the simple side.

The remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a, reversed to rewrite toward the simple side.

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

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

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

Zero to a positive power is zero: 0^(n+1) = 0, reversed to rewrite toward the simple side.

A power of a product is the product of the powers: (a * b)^n = a^n * b^n, reversed to rewrite toward the simple side.

Exponents multiply under repeated powers: a^(m * n) = (a^m)^n, reversed to rewrite toward the simple side.

A common left summand cancels in a difference: (k + n) - (k + m) = n - m, reversed to rewrite toward the simple side.

A common right summand cancels in a difference: (n + k) - (m + k) = n - m, reversed to rewrite toward the simple side.

Multiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k, reversed to rewrite toward the simple side.

Multiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k, reversed to rewrite toward the simple side.

A number is at most the minimum exactly when it is at most both: a <= min b c tests as a <= b and a <= c, reversed to rewrite toward the simple side.

The maximum is at most c exactly when both arguments are: max a b <= c tests as a <= c and 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.