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 (Mathlib's le_min_iff; the implication is le_min_of_le_of_le).

The maximum is at most c exactly when both arguments are: max a b <= c tests as a <= c and b <= c (Mathlib's max_le_iff; the implication is max_le_of_le_of_le).

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.

Every successor is positive: 0 < n + 1.

Below a successor means at most: m < n + 1 tests as m <= n.

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

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

Below a successor is at most: m < n + 1 implies m <= n.

At most is below the successor: m <= n implies m < n + 1.

A strict inequality gives the weak one from the successor: n < m implies n + 1 <= m.

A weak inequality from the successor gives the strict one: n + 1 <= m implies n < m.

The strict order is asymmetric: a < b rules out b < a.

At most means below or equal: a <= b tests as a < b or a = b.

Below means at most and different: a < b tests as a <= b and not a = b.

A natural that does not test equal to zero is positive.

Adding on the right keeps a strict bound: n < m implies n < m + k.

Adding a positive amount on the right strictly increases: n < n + (1 + k).

Adding a positive amount on the left strictly increases: n < (1 + k) + n.

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

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

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

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

A common left summand cancels in a strict inequality: k + a < k + b implies a < b.

A common right summand cancels in a strict inequality: a + k < b + k implies a < b.

Adding two strict bounds keeps a strict bound: a < c and b < d imply a + b < c + d.

A positive left factor never decreases: m <= (1 + n) * m.

A positive right factor never decreases: m <= m * (1 + n).

Multiplying on the left by a positive factor preserves the strict order: a < b implies (1 + k) * a < (1 + k) * b.

Multiplying on the right by a positive factor preserves the strict order: a < b implies a * (1 + k) < b * (1 + k).

A common left factor cancels in a strict inequality: k * a < k * b implies a < b.

A common right factor cancels in a strict inequality: a * k < b * k implies a < b.

Multiplying two strict bounds keeps a strict bound: a < c and b < d imply a * b < c * d.

Squares are monotone: a <= b implies a * a <= b * b.

Squares are strictly monotone: a < b implies a * a < b * b.

Subtracting a positive amount from a positive number decreases it: (1 + n) - (1 + m) < 1 + n.

Subtracting more gives less: n <= m implies k - m <= k - n.

Subtraction on the right preserves the order: n <= m implies n - k <= m - k.

A strict bound on a sum bounds a difference: a + b < c implies a < c - b.

A difference is positive below the minuend: m < n implies 0 < n - m.

Minimum distributes over maximum on the left: min a (max b c) = max (min a b) (min a c).

Maximum distributes over minimum on the left: max a (min b c) = min (max a b) (max a c).

A common left summand leaves the minimum: min (a + b) (a + c) = a + min b c.

A common right summand leaves the minimum: min (a + c) (b + c) = min a b + c.

A common left summand leaves the maximum: max (a + b) (a + c) = a + max b c.

A common right summand leaves the maximum: max (a + c) (b + c) = max a b + c.

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

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

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

A number is at most the maximum exactly when it is at most one argument: a <= max b c tests as a <= b or a <= c.

A bound by the left argument bounds the maximum: a <= b implies a <= max b c.

A bound by the right argument bounds the maximum: a <= c implies a <= max b c.

A bounded left argument bounds the minimum: a <= c implies min a b <= c.

A bounded right argument bounds the minimum: b <= c implies min a b <= c.

Minimum is monotone in both arguments: a <= c and b <= d imply min a b <= min c d.

Maximum is monotone in both arguments: a <= c and b <= d imply max a b <= max c d.

Powers are monotone in the base: a <= b implies a^n <= b^n.

Powers of a positive base are monotone in the exponent: i <= j implies (1 + a)^i <= (1 + a)^j.

Powers of a base above one are strictly monotone in the exponent: i < j implies (2 + a)^i < (2 + a)^j.

Positive powers are strictly monotone in the base: a < b implies a^(1 + n) < b^(1 + n).

Adding a multiple of a positive divisor adds to the quotient: (x + z * (1 + b)) / (1 + b) = x / (1 + b) + z.

Adding a multiple of a positive divisor adds to the quotient: (x + (1 + b) * z) / (1 + b) = x / (1 + b) + z.

Adding a multiple of the divisor keeps the remainder: (a + c * b) % b = a % b.

Adding a multiple of the divisor keeps the remainder: (a + b * c) % b = a % b.

A remainder modulo two is zero or one.

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

Two times n is n + n.

Doubling is multiplying by two: double n = 2 * n.

Doubling distributes over addition: double (a + b) = double a + double b.

Doubling a product doubles its left factor: double (a * b) = double a * b.

Multiplying by a doubled factor doubles the product: a * double b = double (a * b).

Doubling distributes over truncated subtraction: double (a - b) = double a - double b.

A natural is at most its double: n <= double n.

Doubling preserves the order: a <= b implies double a <= double b.

Doubling preserves the strict order: a < b implies double a < double b.

Twice the half plus the parity is the number: double (n / 2) + n % 2 = n.

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

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

Adding the same amount on the right does not change the equality test: a = b tests as a + k = b + k.

Subtracting from the left summand commutes with adding the right one: k <= n implies (n + m) - k = (n - k) + m.

A lower bound of both b and c is a lower bound of their minimum: a <= b and a <= c imply a <= min b c.

An upper bound of both a and b bounds their maximum: a <= c and b <= c imply max a b <= c.

Multiplying n by two gives n + n.

Squaring n gives n times n.

The minimum of two numbers is at most their maximum.

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 (Mathlib's le_min_iff; the implication is le_min_of_le_of_le), 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 (Mathlib's max_le_iff; the implication is max_le_of_le_of_le), reversed to rewrite toward the simple side.

Below a successor means at most: m < n + 1 tests as m <= n, reversed to rewrite toward the simple side.

At most means below or equal: a <= b tests as a < b or a = b, reversed to rewrite toward the simple side.

Below means at most and different: a < b tests as a <= b and not a = b, reversed to rewrite toward the simple side.

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

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

Minimum distributes over maximum on the left: min a (max b c) = max (min a b) (min a c), reversed to rewrite toward the simple side.

Maximum distributes over minimum on the left: max a (min b c) = min (max a b) (max a c), reversed to rewrite toward the simple side.

A common left summand leaves the minimum: min (a + b) (a + c) = a + min b c, reversed to rewrite toward the simple side.

A common right summand leaves the minimum: min (a + c) (b + c) = min a b + c, reversed to rewrite toward the simple side.

A common left summand leaves the maximum: max (a + b) (a + c) = a + max b c, reversed to rewrite toward the simple side.

A common right summand leaves the maximum: max (a + c) (b + c) = max a b + c, reversed to rewrite toward the simple side.

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

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

The maximum is below c exactly when both arguments are: max a b < c tests as a < c and b < c, reversed to rewrite toward the simple side.

A number is at most the maximum exactly when it is at most one argument: a <= max b c tests as a <= b or a <= c, reversed to rewrite toward the simple side.

Adding a multiple of a positive divisor adds to the quotient: (x + z * (1 + b)) / (1 + b) = x / (1 + b) + z, reversed to rewrite toward the simple side.

Adding a multiple of a positive divisor adds to the quotient: (x + (1 + b) * z) / (1 + b) = x / (1 + b) + z, reversed to rewrite toward the simple side.

Adding a multiple of the divisor keeps the remainder: (a + c * b) % b = a % b, reversed to rewrite toward the simple side.

Adding a multiple of the divisor keeps the remainder: (a + b * c) % b = a % b, reversed to rewrite toward the simple side.

A remainder modulo two is zero or one, reversed to rewrite toward the simple side.

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

Two times n is n + n, reversed to rewrite toward the simple side.

Doubling is multiplying by two: double n = 2 * n, reversed to rewrite toward the simple side.

Doubling distributes over addition: double (a + b) = double a + double b, reversed to rewrite toward the simple side.

Doubling a product doubles its left factor: double (a * b) = double a * b, reversed to rewrite toward the simple side.

Multiplying by a doubled factor doubles the product: a * double b = double (a * b), reversed to rewrite toward the simple side.

Doubling distributes over truncated subtraction: double (a - b) = double a - double b, reversed to rewrite toward the simple side.

Twice the half plus the parity is the number: double (n / 2) + n % 2 = n, reversed to rewrite toward the simple side.

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

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

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

Multiplying n by two gives n + n, reversed to rewrite toward the simple side.

Squaring n gives n times n, reversed to rewrite toward the simple side.

The minimum of two numbers is at most their maximum, 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.