bend-mathlib
Releases (15)
Definitions (1,126)
nat.bend
- def internal_div_zero_of_wit
- law div_eq_zero_of_leA number at most b divides by 1 + b to zero: a <= b implies a / (1 + b) = 0.
- def internal_div_le_succ_r
- def internal_div_go_d_ge
- def internal_div_mono_go
- def internal_div_mono_wit
- law div_le_divDivision by a positive divisor is monotone: a <= c implies a / (1 + b) <= c / (1 + b).
- def internal_div_go_shift
- def internal_div_go_run
- law add_div_leftAdding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b).
- def internal_div_le_add_cancel
- def internal_div_gt_add
- def internal_div_not_succ_le
- def internal_div_le_big
- def internal_div_le_small
- def internal_div_le_step
- law le_div_iff_mul_leA quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a.
- law min_commMinimum is commutative.
- law max_commMaximum is commutative.
- law min_selfThe minimum of a natural and itself is itself.
- law max_selfThe maximum of a natural and itself is itself.
- law min_zeroThe minimum with zero is zero: min(a, 0) = 0.
- law zero_minThe minimum with zero is zero: min(0, a) = 0.
- law max_zeroZero is an identity for maximum: max(a, 0) = a.
- law zero_maxZero is an identity for maximum: max(0, a) = a.
- law min_assocMinimum is associative.
- law max_assocMaximum is associative.
- law min_add_maxThe minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b.
- law min_le_leftThe minimum is at most its left argument.
- law min_le_rightThe minimum is at most its right argument.
- law le_max_leftThe left argument is at most the maximum.
- law le_max_rightThe right argument is at most the maximum.
- law pow_zeroAny natural to the power zero is one.
- law pow_succA power with a successor exponent: a^(n+1) = a * a^n.
- law pow_oneAny natural to the power one is itself.
- law one_powOne to any power is one.
- law pow_addExponents add under multiplication: a^(m+n) = a^m * a^n.
- law double_eq_addDoubling is adding a natural to itself.
- law is_eq_reflEvery natural tests equal to itself.
- law is_eq_commThe equality test is symmetric.
- law eq_of_is_eqIf the equality test says true, the naturals are equal.
- law is_ge_eq_is_leA >= b tests the same as b <= a.
- law is_gt_eq_is_ltA > b tests the same as b < a.
- law is_lt_eq_succ_leA < b tests the same as a + 1 <= b.
- law not_is_leNot (a <= b) tests the same as b < a.
- law not_is_ltNot (a < b) tests the same as b <= a.
- law lt_succ_selfEvery natural is less than its successor: n < n + 1.
- law succ_le_succThe successor preserves the order: a <= b implies a + 1 <= b + 1.
- law le_of_succ_le_succThe order of successors is the order of the naturals: a + 1 <= b + 1 implies a <= b.
- law lt_of_lt_of_leA < b and b <= c imply a < c.
- law lt_of_le_of_ltA <= b and b < c imply a < c.
- law add_le_add_leftAdding on the left preserves the order: a <= b implies k + a <= k + b.
- law add_le_add_rightAdding on the right preserves the order: a <= b implies a + k <= b + k.
- law add_le_add_iff_leftAdding the same amount on the left does not change the order test: a <= b tests as k + a <= k + b.
- law add_le_addAdding two bounded summands stays bounded: a <= c and b <= d imply a + b <= c + d.
- law le_and_le_sub_iff_add_leA sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both.
- law le_zero_eqThe only natural at most zero is zero.
- law lt_zeroNo natural is less than zero.
- law not_le_of_ltA strict inequality rules out the reverse weak one: a < b implies b <= a is false.
- law not_lt_of_leA weak inequality rules out the reverse strict one: a <= b implies b < a is false.
- law lt_of_not_leA failed weak test gives the reverse strict order: a <= b false implies b < a.
- law le_of_not_ltA failed strict test gives the reverse weak order: a < b false implies b <= a.
- law lt_minA number below both bounds is below their minimum: a < b and a < c imply a < min b c.
- def internal_or_true_sym
- def internal_or_false_sym
- law min_le_iffThe minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c.
- law lt_max_iffThe maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c.
- law sub_eq_zero_of_leSubtracting a larger number gives zero: a <= b implies a - b = 0.
- law succ_subAbove the subtrahend, a successor subtracts to a successor: b <= a implies (a + 1) - b = (a - b) + 1.
- law add_sub_of_leAdding back what was subtracted restores the number: a <= b implies a + (b - a) = b.
- def internal_lt_sub_zero
- law lt_sub_iff_add_ltComparing against a difference is comparing the sum: a < c - b tests as b + a < c.
- law le_of_add_eqA witnessed difference gives the order: a + k = b implies a <= b.
- law mul_le_mul_rightMultiplying on the right preserves the order: a <= b implies a * k <= b * k.
- law zero_divZero divided by anything is zero: 0 / b = 0.
- law zero_modZero modulo anything is zero: 0 % b = 0.
- def internal_div_go_one
- law div_oneDividing by one changes nothing: a / 1 = a.
- law mod_oneAny natural modulo one is zero: a % 1 = 0.
- def internal_div_go_self
- law mod_selfA natural modulo itself is zero: n % n = 0.
- law div_selfA positive natural divided by itself is one: (1 + b) / (1 + b) = 1.
- def internal_mod_go_le
- law mod_ltA remainder is below its positive divisor: a % (1 + b) < 1 + b.
- law mod_leA remainder never exceeds the dividend: a % b <= a.
- def internal_div_le_self_eq
- law div_le_selfA quotient never exceeds the dividend: a / b <= a.
- def internal_mod_go_small
- def internal_mod_eq_of_wit
- law mod_eq_of_ltA number below the divisor is its own remainder: a < b implies a % b = a.
- law mod_modTaking a remainder twice is taking it once: (a % n) % n = a % n.
- def internal_mod_go_d
- law add_mod_leftAdding the divisor does not change the remainder: (b + a) % b = a % b.
- law mul_div_cancelMultiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a.
- law mul_div_cancel_leftMultiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a.
- law mul_mod_leftA multiple of b leaves no remainder modulo b: (a * b) % b = 0.
- law mul_mod_rightA multiple of a leaves no remainder modulo a: (a * b) % a = 0.
- law mod_add_divThe remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a.
- law div_mul_le_selfThe quotient times the divisor never exceeds the dividend: (a / b) * b <= a.
- law mul_left_commLeft commutativity of multiplication: a * (b * c) = b * (a * c).