Nat.lt_or_gt_of_ne
theorem Nat.lt_or_gt_of_ne : ∀ {a b : ℕ}, a ≠ b → a < b ∨ a > b
This theorem states that for all natural numbers 'a' and 'b', if 'a' is not equal to 'b', then 'a' is either less than 'b' or 'a' is greater than 'b'. It captures a fundamental property of natural numbers, where two distinct numbers must have an order relation where one is less than the other.
More concisely: For all natural numbers a and b, if a ≠ b then a < b or a > b.
|
Nat.succ_add
theorem Nat.succ_add : ∀ (n m : ℕ), n.succ + m = (n + m).succ
This theorem states that for any two natural numbers `n` and `m`, the successor of `n` added to `m` is equal to the successor of the sum of `n` and `m`. In mathematical terms, if `n` and `m` are elements of the natural numbers, then `succ(n) + m = succ(n + m)`. This theorem illustrates a property of the addition operation in natural numbers.
More concisely: For any natural numbers `n` and `m`, `succ(n + m)` equals `succ(n)` plus `m`.
|
Nat.mul_succ
theorem Nat.mul_succ : ∀ (n m : ℕ), n * m.succ = n * m + n
This theorem states that for all natural numbers `n` and `m`, the product of `n` and the successor of `m` (`m` incremented by 1) is equal to the product of `n` and `m` plus `n`. In LaTeX, this would be written as `n * (m + 1) = n * m + n`. This is a property of multiplication over addition in natural numbers, reflecting the distributive law.
More concisely: For all natural numbers `n` and `m`, the product of `n` and the successor of `m` (`m + 1`) equals the sum of `n` times `m` and `n`. In mathematical notation, `n * (m + 1) = n * m + n`.
|
Nat.succ_mul
theorem Nat.succ_mul : ∀ (n m : ℕ), n.succ * m = n * m + m
This theorem states that for any two natural numbers `n` and `m`, the product of the successor of `n` (i.e., `n + 1` in common mathematical notation) and `m` is equal to the sum of the product of `n` and `m`, and `m`. In standard mathematical notation, this is saying that for all natural numbers n and m, (n + 1) * m = n * m + m. This is a basic property of natural number arithmetic, reflecting the distributive law.
More concisely: For all natural numbers n and m, (n + 1) * m = n * m + m.
|
Nat.lt_add_of_pos_right
theorem Nat.lt_add_of_pos_right : ∀ {k n : ℕ}, 0 < k → n < n + k
This theorem states that for any two natural numbers `k` and `n`, if `k` is greater than zero then `n` is less than `n + k`. In other words, adding a positive natural number `k` to another natural number `n` always results in a number that is larger than `n`.
More concisely: For all natural numbers `k` and `n`, if `k > 0` then `n < n + k`.
|
Nat.lt_succ_of_lt
theorem Nat.lt_succ_of_lt : ∀ {a b : ℕ}, a < b → a < b.succ
This theorem states that for all natural numbers `a` and `b`, if `a` is less than `b`, then `a` is also less than `b` incremented by one. This is a basic property of the natural numbers, where increasing a number does not negate previous inequalities.
More concisely: For all natural numbers `a` and `b`, if `a < b` then `a < b + 1`.
|
Nat.add_assoc
theorem Nat.add_assoc : ∀ (n m k : ℕ), n + m + k = n + (m + k)
This theorem, `Nat.add_assoc`, states that for all natural numbers `n`, `m`, and `k`, the operation of addition is associative. In mathematical terms, it states that `(n + m) + k` is equal to `n + (m + k)`. This means that the grouping of addends does not affect the sum.
More concisely: For all natural numbers `n`, `m`, and `k`, `(n + m) + k = n + (m + k)`.
|
Nat.sub_succ_lt_self
theorem Nat.sub_succ_lt_self : ∀ (a i : ℕ), i < a → a - (i + 1) < a - i
This theorem, `Nat.sub_succ_lt_self`, states that for all natural numbers `a` and `i`, if `i` is less than `a`, then the difference between `a` and the successor of `i` is less than the difference between `a` and `i`. Intuitively, incrementing `i` decreases the difference between `a` and `i`, and so `a - (i + 1)` is strictly less than `a - i`.
More concisely: For all natural numbers `a` and `i`, if `i` < `a`, then `a - (i + 1)` < `a - i`.
|
Nat.add_lt_of_lt_sub
theorem Nat.add_lt_of_lt_sub : ∀ {a b c : ℕ}, a < c - b → a + b < c
This theorem states that for any three natural numbers `a`, `b`, and `c`, if `a` is less than the difference of `c` and `b` (`a < c - b`), then the sum of `a` and `b` (`a + b`) is less than `c`. This is essentially a property of natural numbers concerning addition and subtraction.
More concisely: If `a` is smaller than the difference between `c` and `b` (`a < c - b`), then `a + b` is strictly less than `c`.
|
Nat.zero_lt_of_ne_zero
theorem Nat.zero_lt_of_ne_zero : ∀ {a : ℕ}, a ≠ 0 → 0 < a
This theorem states that for any natural number `a`, if `a` is not equal to zero, then zero is less than `a`. In other words, any non-zero natural number is greater than zero.
More concisely: For any natural number `a`, if `a` is non-zero then 0 < `a`.
|
Nat.sub_sub
theorem Nat.sub_sub : ∀ (n m k : ℕ), n - m - k = n - (m + k)
This theorem, `Nat.sub_sub`, states that for all natural numbers `n`, `m`, and `k`, the operation of subtracting `m` and then `k` from `n` is equivalent to subtracting the sum of `m` and `k` from `n`. In mathematical notation, this would be expressed as `n - m - k = n - (m + k)`.
More concisely: For all natural numbers `n`, `m`, and `k`, `n - m - k` equals `n - (m + k)`.
|
Nat.le_of_not_lt
theorem Nat.le_of_not_lt : ∀ {a b : ℕ}, ¬a < b → b ≤ a
This theorem states that for any two natural numbers `a` and `b`, if it is not true that `a` is less than `b`, then `b` must be less than or equal to `a`. In other words, in the natural numbers, not being less than implies being greater than or equal to.
More concisely: If `a` is not less than `b` in the natural numbers, then `b` is less than or equal to `a`.
|
Nat.add_comm
theorem Nat.add_comm : ∀ (n m : ℕ), n + m = m + n
This theorem states that for all natural numbers `n` and `m`, the sum of `n` and `m` is equal to the sum of `m` and `n`. In other words, it asserts the commutative property of addition for natural numbers, that is, the order in which natural numbers are added doesn't affect the result. This can be expressed in LaTeX as: ∀ (n, m ∈ ℕ), n + m = m + n.
More concisely: The theorem asserts the commutativity of natural number addition: for all natural numbers `n` and `m`, `n + m = m + n`.
|
Nat.add_sub_of_le
theorem Nat.add_sub_of_le : ∀ {a b : ℕ}, a ≤ b → a + (b - a) = b
This theorem states that for any two natural numbers `a` and `b`, if `a` is less than or equal to `b`, then adding the difference `b - a` to `a` will yield `b`. In other words, the sum of a number and the difference between a larger (or equal) number and the smaller number is the larger (or equal) number. This is a special case of the more general mathematical principle that adding and then subtracting the same value leaves a number unchanged.
More concisely: For all natural numbers a and b, a + (b - a) = b.
|
Nat.le_of_not_ge
theorem Nat.le_of_not_ge : ∀ {a b : ℕ}, ¬a ≥ b → a ≤ b
This theorem states that for all natural numbers `a` and `b`, if `a` is not greater than or equal to `b`, then `a` must be less than or equal to `b`. In other words, given any two natural numbers, if the first is not at least as large as the second, then it must be no larger than the second.
More concisely: For all natural numbers `a` and `b`, if `a` < `b`, then `a` ≤ `b`.
|
Nat.gt_of_not_le
theorem Nat.gt_of_not_le : ∀ {n m : ℕ}, ¬n ≤ m → n > m
This theorem states that for any two natural numbers `n` and `m`, if it is not the case that `n` is less than or equal to `m`, then `n` must be strictly greater than `m`. In other words, if `n` is not less than or equal to `m` in the natural numbers, the only other possibility is that `n` is greater than `m`.
More concisely: If `n` is not less than or equal to `m` in the natural numbers, then `n` is strictly greater than `m`.
|
Nat.succ_lt_succ
theorem Nat.succ_lt_succ : ∀ {n m : ℕ}, n < m → n.succ < m.succ
This theorem states that for any two natural numbers `n` and `m`, if `n` is less than `m`, then the successor of `n` (or `n + 1`) is less than the successor of `m` (or `m + 1`). This theorem captures the intuitive notion that if one number is smaller than another, then adding the same amount to both does not change the inequality.
More concisely: For all natural numbers `n` and `m`, if `n` < `m`, then `(Suc n)` < `(Suc m)`, where `Suc` denotes the successor function.
|
Nat.le_sub_of_add_le
theorem Nat.le_sub_of_add_le : ∀ {a b c : ℕ}, a + b ≤ c → a ≤ c - b
This theorem states that for any three natural numbers `a`, `b`, and `c`, if the sum of `a` and `b` is less than or equal to `c`, then `a` is less than or equal to the difference of `c` and `b`. In mathematical notation, this theorem can be expressed as: if $a + b \leq c$, then $a \leq c - b$.
More concisely: If $a$, $b$, and $c$ are natural numbers with $a + b \leq c$, then $a \leq c - b$.
|
Nat.succ_inj'
theorem Nat.succ_inj' : ∀ {a b : ℕ}, a.succ = b.succ ↔ a = b
This theorem, `Nat.succ_inj'`, states that for any two natural numbers `a` and `b`, the successor of `a` is equal to the successor of `b` if and only if `a` is equal to `b`. In other words, it guarantees the injectivity of the successor function on natural numbers: different natural numbers will have different successors.
More concisely: The successor function is injective on natural numbers: for all natural numbers a and b, if succ(a) = succ(b), then a = b.
|
Nat.mul_add
theorem Nat.mul_add : ∀ (n m k : ℕ), n * (m + k) = n * m + n * k
This theorem states that for all natural numbers `n`, `m`, and `k`, the product of `n` and the sum of `m` and `k` is equal to the sum of the product of `n` and `m` and the product of `n` and `k`. In mathematical terms, it expresses the distributive property of multiplication over addition for natural numbers: `n*(m+k) = n*m + n*k`.
More concisely: For all natural numbers `n`, `m`, and `k`, the product of `n` with the sum of `m` and `k` is equal to the sum of the products of `n` with `m` and `k` (distributive property of multiplication over addition).
|
Nat.lt_of_succ_le
theorem Nat.lt_of_succ_le : ∀ {n m : ℕ}, n.succ ≤ m → n < m
This theorem, `Nat.lt_of_succ_le`, states that for any two natural numbers `n` and `m`, if the successor of `n` (which is `n + 1`) is less than or equal to `m`, then `n` is strictly less than `m`. This is a basic property of natural numbers, encapsulating the intuitive idea that if `n + 1` is not greater than `m`, then `n` must be less than `m`.
More concisely: If `n + 1 ≤ m`, then `n < m` for natural numbers `n` and `m`.
|
Nat.succ_le_of_lt
theorem Nat.succ_le_of_lt : ∀ {n m : ℕ}, n < m → n.succ ≤ m
This theorem, `Nat.succ_le_of_lt`, states that for any two natural numbers `n` and `m`, if `n` is less than `m`, then the successor of `n` (which is `n + 1`) is less than or equal to `m`. In other words, it expresses that if one natural number is strictly smaller than another, then the next natural number will be either still smaller or exactly equal to the second number. This is a fundamental property of the natural number ordering.
More concisely: For all natural numbers `n` and `m`, if `n` < `m`, then `nat.succ n` ≤ `m`.
|
Nat.add_right_cancel
theorem Nat.add_right_cancel : ∀ {n m k : ℕ}, n + m = k + m → n = k
This theorem, `Nat.add_right_cancel`, states that for all natural numbers `n`, `m`, and `k`, if the sum of `n` and `m` equals the sum of `k` and `m`, then `n` must equal `k`. Essentially, it ensures that addition on the right side of a natural number is "cancelable", which is a crucial property of addition in the context of natural numbers.
More concisely: If `n + m = k + m`, then `n = k`.
|
Nat.pos_of_ne_zero
theorem Nat.pos_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → 0 < n
This theorem, `Nat.pos_of_ne_zero`, states that for any natural number `n`, if `n` is not equal to zero, then `n` is greater than zero. In other words, a non-zero natural number is always positive.
More concisely: For any natural number `n`, `n` is positive if and only if `n` is not zero.
|
Nat.sub_self
theorem Nat.sub_self : ∀ (n : ℕ), n - n = 0
This theorem states that for every natural number `n`, the result of subtracting `n` from itself is zero. In other words, any natural number minus itself always equals zero.
More concisely: For all natural numbers n, n - n = 0.
|
Nat.not_lt
theorem Nat.not_lt : ∀ {a b : ℕ}, ¬a < b ↔ b ≤ a
This theorem states that for all natural numbers `a` and `b`, the negation of `a` being less than `b` is equivalent to `b` being less than or equal to `a`. In other words, if it is not true that `a` is less than `b`, then `b` must be less than or equal to `a`.
More concisely: For all natural numbers `a` and `b`, `~(a < b)` is equivalent to `b <= a`.
|
Nat.add_succ
theorem Nat.add_succ : ∀ (n m : ℕ), n + m.succ = (n + m).succ
This theorem states that for all natural numbers `n` and `m`, the sum of `n` and the successor of `m` (which is `m + 1`) is equal to the successor of the sum of `n` and `m` (which is `n + m + 1`). In other words, adding `n` to `m + 1` is the same as adding `n + m` to `1`. This property is foundational to the definition of addition in the natural numbers.
More concisely: For all natural numbers `n` and `m`, `(n + (m + 1)) = (n + m + 1)`.
|
Nat.not_lt_of_ge
theorem Nat.not_lt_of_ge : ∀ {a b : ℕ}, b ≥ a → ¬b < a
This theorem states that for any two natural numbers, `a` and `b`, if `b` is greater than or equal to `a`, then it is not possible for `b` to be less than `a`. It captures the logical and mathematical principle that a number cannot simultaneously be greater than or equal to, and less than, another number.
More concisely: For all natural numbers `a` and `b`, if `b` is greater than or equal to `a`, then it is not the case that `a` is greater than `b`.
|
Nat.succ_sub
theorem Nat.succ_sub : ∀ {m n : ℕ}, n ≤ m → m.succ - n = (m - n).succ
This theorem states that for all natural numbers `m` and `n`, if `n` is less than or equal to `m`, then subtracting `n` from the successor of `m` (i.e., `m` plus one, or `Nat.succ m`) is equal to the successor of `m - n`. In mathematical terms, the theorem can be expressed as ∀m, n ∈ ℕ, n ≤ m → (m+1) - n = (m - n) + 1.
More concisely: For all natural numbers `m` and `n`, if `n` lever equals `m`, then `(m + 1) - n = (m - n) + 1`.
|
Nat.succ_le_succ_iff
theorem Nat.succ_le_succ_iff : ∀ {a b : ℕ}, a.succ ≤ b.succ ↔ a ≤ b
This theorem states that for any two natural numbers 'a' and 'b', the successor of 'a' is less than or equal to the successor of 'b' if and only if 'a' is less than or equal to 'b'. In other words, incrementing both 'a' and 'b' by 1 does not change their relative ordering.
More concisely: For any natural numbers 'a' and 'b', the successor of 'a' is less than or equal to the successor of 'b' if and only if 'a' is less than or equal to 'b'. Equivalently, a + 1 ≤ b + 1 if and only if a ≤ b.
|
Nat.mul_sub_left_distrib
theorem Nat.mul_sub_left_distrib : ∀ (n m k : ℕ), n * (m - k) = n * m - n * k
This theorem is stating a property of natural numbers with respect to multiplication and subtraction. Specifically, it states that for any three natural numbers `n`, `m`, and `k`, the product of `n` and the difference between `m` and `k` (i.e., `n * (m - k)`) is equal to the difference between the product of `n` and `m` and the product of `n` and `k` (i.e., `n * m - n * k`). This is known as the distributive property of multiplication over subtraction.
More concisely: For all natural numbers `n`, `m`, and `k`, `n * (m - k)` equals `n * m - n * k`.
|
Nat.succ_eq_add_one
theorem Nat.succ_eq_add_one : ∀ (n : ℕ), n.succ = n + 1
This theorem states that for every natural number `n`, the successor of `n` is equal to `n` plus one. In other words, it enforces the standard mathematical principle that adding one to a natural number gives you the next consecutive natural number.
More concisely: For every natural number `n`, `(Suc n) = n + 1`.
|
Nat.pred_le
theorem Nat.pred_le : ∀ (n : ℕ), n.pred ≤ n
This theorem states that for any natural number `n`, the predecessor of `n` is less than or equal to `n`. The predecessor of a natural number `n` is defined as `n - 1` or `0` if `n` is `0`. The theorem thus captures the intuitive idea that a number is always greater than or equal to its predecessor.
More concisely: For all natural numbers n, 0 <= pred n, where pred denotes the predecessor function.
|
Nat.sub_le_sub_left
theorem Nat.sub_le_sub_left : ∀ {n m : ℕ}, n ≤ m → ∀ (k : ℕ), k - m ≤ k - n
This theorem states that for any three natural numbers `n`, `m` and `k`, if `n` is less than or equal to `m`, then the result of subtracting `m` from `k` is less than or equal to the result of subtracting `n` from `k`. In mathematical terms, this can be written as: if n ≤ m, then k - m ≤ k - n for all natural numbers n, m, and k. Essentially, subtracting a larger number from `k` results in a smaller value.
More concisely: For all natural numbers n, m, and k, if n <= m then k - m <= k - n.
|
Nat.sub_ne_zero_of_lt
theorem Nat.sub_ne_zero_of_lt : ∀ {a b : ℕ}, a < b → b - a ≠ 0
This theorem states that for any two natural numbers `a` and `b`, if `a` is less than `b`, then the result of subtracting `a` from `b` cannot be zero. This means there is no circumstance where a smaller number can be subtracted from a larger number to result in zero in the domain of natural numbers.
More concisely: For all natural numbers `a` and `b`, if `a < b`, then `b - a` is a positive natural number.
|
Nat.sub_lt_left_of_lt_add
theorem Nat.sub_lt_left_of_lt_add : ∀ {n k m : ℕ}, n ≤ k → k < n + m → k - n < m
This theorem, `Nat.sub_lt_left_of_lt_add`, states that for any three natural numbers `n`, `k`, and `m`, if `n` is less than or equal to `k`, and `k` is less than the sum of `n` and `m`, then the result of the subtraction of `n` from `k` is less than `m`. In mathematical terms, given that $n \leq k$ and $k < n + m$, it ensures that $k - n < m$.
More concisely: If $n \leq k$ and $k < n + m$, then $k - n < m$.
|
Nat.le_add_right
theorem Nat.le_add_right : ∀ (n k : ℕ), n ≤ n + k
This theorem states that for all natural numbers `n` and `k`, `n` is less than or equal to `n + k`. In mathematical terms, this theorem confirms that adding any natural number to another natural number results in a number that is either greater than or equal to the original number. It's an important foundational aspect of number theory and arithmetic.
More concisely: For all natural numbers `n` and `k`, `n ≤ n + k`.
|
Nat.sub_le_sub_right
theorem Nat.sub_le_sub_right : ∀ {n m : ℕ}, n ≤ m → ∀ (k : ℕ), n - k ≤ m - k
This theorem states that for any three natural numbers `n`, `m`, and `k`, if `n` is less than or equal to `m`, then the difference between `n` and `k` is also less than or equal to the difference between `m` and `k`. In mathematical terms, if `n ≤ m`, then `n - k ≤ m - k` for any `k`. This is a fundamental property of subtraction in the natural numbers.
More concisely: For all natural numbers `n`, `m`, and `k`, if `n ≤ m`, then `n - k ≤ m - k`.
|
Nat.sub_le
theorem Nat.sub_le : ∀ (n m : ℕ), n - m ≤ n
This theorem states that for any two natural numbers `n` and `m`, the difference `n - m` is less than or equal to `n`. Essentially, it captures the idea that subtracting any value from a natural number can never result in a number greater than the original number.
More concisely: For all natural numbers n and m, n - m <= n.
|
Nat.lt_of_sub_eq_succ
theorem Nat.lt_of_sub_eq_succ : ∀ {m n l : ℕ}, m - n = l.succ → n < m
This theorem states that for any three natural numbers `m`, `n`, and `l`, if the difference between `m` and `n` equals the successor (or `l + 1`) of `l`, it follows that `n` is less than `m`. In other words, if `m - n` gives a positive result (the successor of some natural number `l`), then `m` must be greater than `n`.
More concisely: If `m` and `n` are natural numbers such that `m = l + 1 + n`, then `m > n`.
|
Nat.zero_lt_two
theorem Nat.zero_lt_two : 0 < 2
This theorem states that zero is less than two in the domain of natural numbers. In other words, it confirms the mathematical fact that the natural number 0 is indeed smaller than the natural number 2.
More concisely: The theorem asserts that 0 < 2 in the natural numbers.
|
Nat.not_le_of_lt
theorem Nat.not_le_of_lt : ∀ {a b : ℕ}, a < b → ¬b ≤ a
This theorem states that for any two natural numbers `a` and `b`, if `a` is less than `b`, then it is not possible for `b` to be less than or equal to `a`. In other words, the comparative relation of 'less than' between two numbers excludes the possibility of the other number being 'less than or equal to' the first. This makes sense intuitively, as a number cannot be both larger and smaller or equal to another number at the same time.
More concisely: For all natural numbers `a` and `b`, if `a` < `b`, then it is not the case that `b` <= `a`.
|
Nat.lt_of_lt_of_le
theorem Nat.lt_of_lt_of_le : ∀ {n m k : ℕ}, n < m → m ≤ k → n < k
This theorem, `Nat.lt_of_lt_of_le`, states that for any three natural numbers `n`, `m`, and `k`, if `n` is less than `m` and `m` is less than or equal to `k`, then `n` is less than `k`. Essentially, it expresses a property of the order of natural numbers: the transitivity of the less than relation through a less than or equal relation.
More concisely: If `n` is less than `m` and `m` is less than or equal to `k`, then `n` is less than `k`. (Transitivity of the less than relation through a less than or equal relation in the context of natural numbers.)
|
Nat.add_lt_add
theorem Nat.add_lt_add : ∀ {a b c d : ℕ}, a < b → c < d → a + c < b + d
This theorem states that for all natural numbers `a`, `b`, `c`, and `d`, if `a` is less than `b` and `c` is less than `d`, then `a + c` is less than `b + d`. In other words, the sum of two smaller natural numbers is less than the sum of two larger natural numbers.
More concisely: For all natural numbers `a`, `b`, `c`, and `d`, if `a < b` and `c < d`, then `a + c < b + d`.
|
Nat.lt.base
theorem Nat.lt.base : ∀ (n : ℕ), n < n.succ
This theorem, `Nat.lt.base`, states that for every natural number `n`, `n` is less than its successor (`n + 1`). In other words, any natural number is always less than the next natural number.
More concisely: For all natural numbers n, n < n + 1.
|
Nat.mul_le_mul
theorem Nat.mul_le_mul : ∀ {n₁ m₁ n₂ m₂ : ℕ}, n₁ ≤ n₂ → m₁ ≤ m₂ → n₁ * m₁ ≤ n₂ * m₂
This theorem states that for all natural numbers `n₁`, `m₁`, `n₂`, `m₂`, if `n₁` is less than or equal to `n₂` and `m₁` is less than or equal to `m₂`, then the product of `n₁` and `m₁` is also less than or equal to the product of `n₂` and `m₂`. This is a property of multiplication in the set of natural numbers.
More concisely: For all natural numbers `n₁`, `m₁`, `n₂`, `m₂`, if `n₁ ≤ n₂` and `m₁ ≤ m₂`, then `n₁ * m₁ ≤ n₂ * m₂`.
|
Nat.add_le_of_le_sub
theorem Nat.add_le_of_le_sub : ∀ {a b c : ℕ}, b ≤ c → a ≤ c - b → a + b ≤ c
This theorem, `Nat.add_le_of_le_sub`, states that for any natural numbers `a`, `b`, and `c`, if `b` is less than or equal to `c` (`b ≤ c`) and `a` is less than or equal to the difference of `c` and `b` (`a ≤ c - b`), then the sum of `a` and `b` is less than or equal to `c` (`a + b ≤ c`). In other words, if a natural number is at most the difference of two others, then its sum with one of those numbers is at most the larger number.
More concisely: If `a` is a natural number and `b` and `c` are natural numbers with `b <= c` and `a <= c - b`, then `a + b <= c`.
|
Nat.not_eq_zero_of_lt
theorem Nat.not_eq_zero_of_lt : ∀ {b a : ℕ}, b < a → a ≠ 0
This theorem states that for any two natural numbers `a` and `b`, if `b` is less than `a`, then `a` cannot be zero. This is because zero is the smallest natural number and if `b` is less than `a`, then `a` must be greater than zero.
More concisely: For all natural numbers `a` and `b`, if `b` < `a`, then `a` is non-zero.
|
Nat.zero_eq
theorem Nat.zero_eq : Nat.zero = 0
This theorem states that the natural number zero, denoted as `Nat.zero` in Lean, is equal to the numeral `0`. Although they may appear to be defined differently in the context of the Lean programming language, this theorem assures us that they are indeed the same value.
More concisely: The theorem asserts the equality of the natural number zero in Lean and the numeral 0.
|
Nat.add_le_add
theorem Nat.add_le_add : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → a + c ≤ b + d
This theorem states that for any four natural numbers `a`, `b`, `c`, and `d`, if `a` is less than or equal to `b` and `c` is less than or equal to `d`, then the sum of `a` and `c` is less than or equal to the sum of `b` and `d`. This property is a key aspect of the order-preserving nature of addition in the natural numbers.
More concisely: For all natural numbers a, b, c, and d, if a ≤ b and c ≤ d then a + c ≤ b + d.
|
Nat.pos_iff_ne_zero
theorem Nat.pos_iff_ne_zero : ∀ {n : ℕ}, 0 < n ↔ n ≠ 0
This theorem, `Nat.pos_iff_ne_zero`, states that for any natural number `n`, `n` is greater than 0 if and only if `n` is not equal to 0. In mathematical terms, this means ∀ n ∈ ℕ, n > 0 ↔ n ≠ 0.
More concisely: A natural number is positive if and only if it is not zero. (Equivalently, n > 0 if and only if n ≠ 0.)
|
Nat.ne_of_lt
theorem Nat.ne_of_lt : ∀ {a b : ℕ}, a < b → a ≠ b
This theorem states that for all natural numbers 'a' and 'b', if 'a' is less than 'b', then 'a' is not equal to 'b'. This is a fundamental property in the number theory of natural numbers, asserting that a smaller number cannot be equal to a larger number.
More concisely: For all natural numbers a and b, if a < b then a ≠ b.
|
Nat.add_le_add_right
theorem Nat.add_le_add_right : ∀ {n m : ℕ}, n ≤ m → ∀ (k : ℕ), n + k ≤ m + k
This theorem states that for any natural numbers `n`, `m`, and `k`, if `n` is less than or equal to `m`, then `n + k` is also less than or equal to `m + k`. In other words, adding the same number `k` to both sides of an inequality between natural numbers does not change the truth of the inequality.
More concisely: For all natural numbers `n`, `m`, and `k`, if `n ≤ m`, then `n + k ≤ m + k`.
|
Nat.zero_sub
theorem Nat.zero_sub : ∀ (n : ℕ), 0 - n = 0
This theorem in Lean 4 states that for any natural number 'n', the result of subtracting 'n' from zero is always zero. In other words, it formalizes the mathematical concept that $0 - n = 0$ for all natural numbers 'n'.
More concisely: For all natural numbers n, 0 - n = 0.
|
Nat.sub_eq_iff_eq_add
theorem Nat.sub_eq_iff_eq_add : ∀ {b a c : ℕ}, b ≤ a → (a - b = c ↔ a = c + b)
This theorem states that for any three natural numbers `a`, `b`, and `c`, if `b` is less than or equal to `a`, then the difference of `a` and `b` equals `c` if and only if `a` equals `c` plus `b`. In other words, the difference between `a` and `b` being `c` is equivalent to `c` added to `b` resulting in `a`. This theorem essentially provides an equivalence between subtraction and addition operations under certain conditions on natural numbers.
More concisely: For natural numbers `a`, `b`, and `c`, `a = c + b` if and only if `b <= a` and `a = c + b`.
|
Nat.add_lt_add_left
theorem Nat.add_lt_add_left : ∀ {n m : ℕ}, n < m → ∀ (k : ℕ), k + n < k + m
This theorem states that for all natural numbers `n` and `m`, if `n` is less than `m`, then for any natural number `k`, the sum of `k` and `n` is less than the sum of `k` and `m`. In simpler terms, it asserts that adding a constant to both sides of a valid inequality between natural numbers preserves the inequality.
More concisely: For all natural numbers `n` and `m` with `n < m`, for any natural number `k`, `k + n < k + m`.
|
Nat.exists_eq_succ_of_ne_zero
theorem Nat.exists_eq_succ_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → ∃ k, n = k.succ
This theorem states that for any natural number `n` that is not zero, there exists another natural number `k` such that `n` is the successor of `k`. In other words, if you have a nonzero natural number, it must be one greater than another natural number.
More concisely: For any non-zero natural number `n`, there exists a natural number `k` such that `n = Succ(k)`.
|
Nat.ge_of_not_lt
theorem Nat.ge_of_not_lt : ∀ {n m : ℕ}, ¬n < m → n ≥ m
This theorem, `Nat.ge_of_not_lt`, states that for any two natural numbers `n` and `m`, if it is not the case that `n` is less than `m` (`¬n < m`), then `n` must be greater than or equal to `m` (`n ≥ m`). This is a basic property of ordered number systems like the natural numbers, and it captures the idea that if one number isn't less than another, then it must be either equal to or greater than the other number.
More concisely: If `n` is not less than `m` (`¬n < m`), then `n` is greater than or equal to `m` (`n ≥ m`).
|
Nat.succ_pred_eq_of_pos
theorem Nat.succ_pred_eq_of_pos : ∀ {n : ℕ}, 0 < n → n.pred.succ = n
This theorem, `Nat.succ_pred_eq_of_pos`, states that for all natural numbers `n`, if `n` is greater than `0`, then the successor of the predecessor of `n` is equal to `n` itself. In other words, if we have a positive natural number `n`, decrementing it by 1 (using `Nat.pred`) and then incrementing it by 1 (using `Nat.succ`) returns us back to the original number `n`.
More concisely: For all natural numbers `n` greater than 0, `Nat.succ (Nat.pred n) = n`.
|
Nat.lt_succ_of_le
theorem Nat.lt_succ_of_le : ∀ {n m : ℕ}, n ≤ m → n < m.succ
This theorem, `Nat.lt_succ_of_le`, states that for any two natural numbers `n` and `m`, if `n` is less than or equal to `m`, then `n` is less than the successor of `m` (i.e., `m+1`). In other words, if a natural number `n` is not greater than another natural number `m`, then `n` is definitely less than `m+1`.
More concisely: For all natural numbers `n` and `m`, if `n ≤ m`, then `n < m + 1`.
|
Nat.succ_lt_succ_iff
theorem Nat.succ_lt_succ_iff : ∀ {a b : ℕ}, a.succ < b.succ ↔ a < b
This theorem states that for any two natural numbers 'a' and 'b', the successor of 'a' (i.e., 'a+1') is less than the successor of 'b' (i.e., 'b+1') if and only if 'a' is less than 'b'. It essentially asserts that adding 1 to both sides of an inequality between natural numbers doesn't change the validity of the inequality.
More concisely: For all natural numbers a and b, a < b if and only if a + 1 < b + 1.
|
Nat.sub_succ
theorem Nat.sub_succ : ∀ (n m : ℕ), n - m.succ = (n - m).pred
The theorem `Nat.sub_succ` is a statement about subtraction and the predecessor function on natural numbers. For all natural numbers `n` and `m`, the difference between `n` and the successor of `m` (`Nat.succ m` which represents `m+1`) is the same as the predecessor (`Nat.pred`) of the difference between `n` and `m`. In other words, if we subtract `m+1` from `n`, it's the same as first subtracting `m` from `n` and then taking the predecessor of that result. This theorem formalizes one of the basic properties of subtraction on natural numbers.
More concisely: For all natural numbers `n` and `m`, `n - Nat.succ m = Nat.pred (n - m)`.
|
Nat.sub_lt_sub_left
theorem Nat.sub_lt_sub_left : ∀ {k m n : ℕ}, k < m → k < n → m - n < m - k
This theorem states that for any three natural numbers `k`, `m`, and `n`, if `k` is less than `m` and `k` is less than `n`, then the difference of `m` and `n` is less than the difference of `m` and `k`. In other words, it expresses that subtracting a larger number from `m` results in a smaller result than subtracting a smaller number from `m`, given the ordering constraint on `k`, `m`, and `n`. This is a property of subtraction in the set of natural numbers.
More concisely: For natural numbers `k`, `m`, and `n`, if `k` < `m` and `k` < `n`, then `m - k` < `m - n`.
|
Nat.sub_add_eq
theorem Nat.sub_add_eq : ∀ (a b c : ℕ), a - (b + c) = a - b - c
This theorem, `Nat.sub_add_eq`, states that for all natural numbers `a`, `b`, and `c`, the result of subtracting the sum of `b` and `c` from `a` is the same as the result of subtracting `c` from the difference of `a` and `b`. In mathematical notation, this would be expressed as `a - (b + c) = a - b - c`.
More concisely: For all natural numbers `a`, `b`, and `c`, `a - (b + c) = a - b - c`.
|
Nat.pred_eq_sub_one
theorem Nat.pred_eq_sub_one : ∀ {n : ℕ}, n.pred = n - 1
This theorem, `Nat.pred_eq_sub_one`, states that for every natural number `n`, the predecessor function `Nat.pred n` is equivalent to `n - 1`. In other words, applying the predecessor function to any natural number yields the same result as subtracting 1 from that number.
More concisely: For all natural numbers n, Nat.pred n = n - 1.
|
Nat.pred_lt
theorem Nat.pred_lt : ∀ {n : ℕ}, n ≠ 0 → n.pred < n
This theorem states that for any natural number `n`, if `n` is not equal to zero, then the predecessor of `n` (denoted as `Nat.pred n`), is strictly less than `n`. Recall that the predecessor of a natural number `n` is obtained by subtracting one from `n`, but when `n` is zero, the predecessor is defined to be zero as well. Thus, this theorem is asserting that any non-zero natural number is strictly greater than its predecessor.
More concisely: For any natural number `n` different from zero, `Nat.pred n` is strictly less than `n`.
|
Nat.lt_of_not_ge
theorem Nat.lt_of_not_ge : ∀ {a b : ℕ}, ¬b ≥ a → b < a
This theorem states that for all natural numbers `a` and `b`, if it is not true that `b` is greater than or equal to `a`, then `b` must be less than `a`. In essence, this theorem is expressing a basic property of the ordering of natural numbers: the only alternative to `b` being greater than or equal to `a` is that `b` is less than `a`.
More concisely: For all natural numbers `a` and `b`, if `b` is not greater than or equal to `a`, then `b` is less than `a`.
|
Init.Data.Nat.Basic._auxLemma.1
theorem Init.Data.Nat.Basic._auxLemma.1 : ∀ (n : ℕ), (0 ≤ n) = True
This theorem states that for any natural number `n`, the statement "0 is less than or equal to `n`" is always true. This is a basic property of natural numbers in mathematical principles, where 0 is the minimum value and every natural number is either this minimum value or greater.
More concisely: For all natural numbers n, 0 ≤ n.
|
Nat.le_of_succ_le
theorem Nat.le_of_succ_le : ∀ {n m : ℕ}, n.succ ≤ m → n ≤ m
This theorem states that for any two natural numbers `n` and `m`, if the successor of `n` (which is `n + 1`) is less than or equal to `m`, then `n` is also less than or equal to `m`. In other words, if `n + 1 ≤ m`, then it must be the case that `n ≤ m`. This is a basic property of natural numbers and order relations.
More concisely: If `n + 1 ≤ m`, then `n ≤ m`.
|
Nat.pow_zero
theorem Nat.pow_zero : ∀ (n : ℕ), n ^ 0 = 1
This theorem states that any natural number raised to the power of zero is equal to one. That is, for any natural number 'n', 'n' to the power of 0 is 1. This is consistent with the mathematical law that any non-zero number raised to the power of zero equals one.
More concisely: For all natural numbers n, n^0 = 1.
|
Nat.add_sub_self_left
theorem Nat.add_sub_self_left : ∀ (a b : ℕ), a + b - a = b
This theorem states that for any two natural numbers `a` and `b`, if we add `a` and `b` together and then subtract `a` from the result, we will be left with `b`. In mathematical terms, it represents the equation `a + b - a = b` for all natural numbers `a` and `b`.
More concisely: For all natural numbers `a` and `b`, `a + b = a + b - a + a ↔ b`.
|
Nat.add_lt_add_right
theorem Nat.add_lt_add_right : ∀ {n m : ℕ}, n < m → ∀ (k : ℕ), n + k < m + k
This theorem states that for all natural numbers `n`, `m`, and `k`, if `n` is less than `m`, then the sum of `n` and `k` is less than the sum of `m` and `k`. In other words, if one natural number is smaller than another, adding the same value to both will maintain the order.
More concisely: For all natural numbers `n`, `m`, and `k`, if `n` < `m` then `n + k` < `m + k`.
|
Nat.add_left_comm
theorem Nat.add_left_comm : ∀ (n m k : ℕ), n + (m + k) = m + (n + k)
This theorem is called `Nat.add_left_comm`, and it states that for any three natural numbers `n`, `m`, and `k`, the sum of `n` and the sum of `m` and `k` is equal to the sum of `m` and the sum of `n` and `k`. In other words, it's saying that addition of natural numbers is left-commutative. This could be written in mathematical notation as ∀ n, m, k ∈ ℕ, n + (m + k) = m + (n + k).
More concisely: For all natural numbers `n`, `m`, and `k`, the left-commutative property holds for addition, that is, `n + (m + k) = m + (n + k)`.
|
Nat.le_of_eq
theorem Nat.le_of_eq : ∀ {n m : ℕ}, n = m → n ≤ m
This theorem, `Nat.le_of_eq`, asserts that for any two natural numbers `n` and `m`, if `n` equals `m`, then `n` is less than or equal to `m`. This is a fundamental property of the natural numbers, and the inequality relationship, where an equality between two numbers implies a less-than-or-equal-to relationship between the same two numbers.
More concisely: For all natural numbers n and m, if n = m then n ≤ m.
|
Nat.zero_lt_of_lt
theorem Nat.zero_lt_of_lt : ∀ {a b : ℕ}, a < b → 0 < b
This theorem, `Nat.zero_lt_of_lt`, states that for any two natural numbers `a` and `b`, if `a` is less than `b`, then `0` is less than `b`. Essentially, it asserts that if a natural number is greater than any other natural number, then it must be greater than zero.
More concisely: For all natural numbers `a` and `b`, if `a` < `b`, then 0 < `b`.
|
Nat.eq_zero_or_pos
theorem Nat.eq_zero_or_pos : ∀ (n : ℕ), n = 0 ∨ n > 0
This theorem states that for every natural number `n`, `n` is either equal to zero or greater than zero. In other words, it asserts that any natural number is either zero or a positive integer. This is a fundamental property of natural numbers in the standard mathematical system.
More concisely: Every natural number is non-negative. (Or, every natural number is greater than or equal to zero.)
|
Nat.pow_le_pow_of_le_left
theorem Nat.pow_le_pow_of_le_left : ∀ {n m : ℕ}, n ≤ m → ∀ (i : ℕ), n ^ i ≤ m ^ i
This theorem states that for any natural numbers `n` and `m`, if `n` is less than or equal to `m`, then `n` to the power of any natural number `i` is also less than or equal to `m` to the power of `i`. In other words, it generalizes the property of order preservation under exponentiation for natural numbers.
More concisely: For all natural numbers `n` and `m` and `i`, if `n <= m`, then `n^i <= m^i`.
|
Nat.mul_zero
theorem Nat.mul_zero : ∀ (n : ℕ), n * 0 = 0
This theorem states that for any natural number `n`, the multiplication of `n` and `0` is `0`. In other words, any natural number multiplied by zero gives zero. This is a fundamental property of multiplication in the set of natural numbers (ℕ).
More concisely: For all natural numbers n, n × 0 = 0.
|
Nat.not_lt_of_le
theorem Nat.not_lt_of_le : ∀ {a b : ℕ}, a ≤ b → ¬b < a
This theorem states that for any two natural numbers `a` and `b`, if `a` is less than or equal to `b`, then `b` cannot be less than `a`. In other words, it's impossible for `b` to be less than `a` if `a` is already less than or equal to `b`. This is a basic principle of order in the set of natural numbers.
More concisely: For all natural numbers `a` and `b`, if `a ≤ b`, then `b` cannot be less than `a` (i.e., `a < b` is false).
|
Nat.add_le_add_left
theorem Nat.add_le_add_left : ∀ {n m : ℕ}, n ≤ m → ∀ (k : ℕ), k + n ≤ k + m
This theorem, "Nat.add_le_add_left", in Lean 4 states that for all natural numbers 'n' and 'm', if 'n' is less than or equal to 'm', then for any natural number 'k', the sum of 'k' and 'n' is less than or equal to the sum of 'k' and 'm'. Essentially, it provides a guarantee that adding a constant to both sides of a valid inequality between natural numbers will not alter the inequality's truth.
More concisely: For all natural numbers n, m, and k, if n ≤ m then n + k ≤ m + k.
|
Nat.sub_eq_zero_of_le
theorem Nat.sub_eq_zero_of_le : ∀ {n m : ℕ}, n ≤ m → n - m = 0
This theorem states that for any two natural numbers `n` and `m`, if `n` is less than or equal to `m`, then the result of `n - m` equals 0. In mathematical terms, it asserts that for all `n, m` in the set of natural numbers ℕ, if `n ≤ m`, then `n - m = 0`. In essence, it captures the mathematical fact that subtracting a larger number from a smaller or equal one in the set of natural numbers yields zero.
More concisely: For all natural numbers `n` and `m`, if `n ≤ m`, then `n - m = 0`.
|
Nat.lt_succ_iff_lt_or_eq
theorem Nat.lt_succ_iff_lt_or_eq : ∀ {m n : ℕ}, m < n.succ ↔ m < n ∨ m = n
This theorem states that for any two natural numbers `m` and `n`, `m` is less than the successor of `n` if and only if `m` is either less than `n` or equal to `n`. In the context of natural numbers, the successor of a number `n` is simply `n + 1`. Hence, this theorem essentially provides a condition for when a number is less than or equal to another number.
More concisely: For natural numbers `m` and `n`, `m` is less than `n + 1` if and only if `m` is less than or equal to `n`.
|
Nat.eq_add_of_sub_eq
theorem Nat.eq_add_of_sub_eq : ∀ {a b c : ℕ}, b ≤ a → a - b = c → a = c + b
This theorem states that for any three natural numbers `a`, `b`, and `c`, if `b` is less than or equal to `a`, and the difference of `a` and `b` is equal to `c`, then `a` is equal to the sum of `c` and `b`. In other words, it is expressing the property of subtraction and its relationship to addition in the natural numbers, namely if you subtract `b` from `a` to get `c`, you can add `b` back to `c` to get `a` again.
More concisely: For natural numbers `a`, `b`, and `c`, if `b` ≤ `a` and `a` = `b` + `c`, then `a` = `c` + `b`.
|
Nat.le_total
theorem Nat.le_total : ∀ (m n : ℕ), m ≤ n ∨ n ≤ m
This theorem, `Nat.le_total`, states that for any two natural numbers `m` and `n`, either `m` is less than or equal to `n`, or `n` is less than or equal to `m`. This is a formal statement of the total ordering of the natural numbers, ensuring that given any two natural numbers, they are either equal or one is greater than the other.
More concisely: For all natural numbers m and n, either m ≤ n or n ≤ m.
|
Nat.sub_eq_of_eq_add
theorem Nat.sub_eq_of_eq_add : ∀ {a b c : ℕ}, a = c + b → a - b = c
This theorem states that for any three natural numbers `a`, `b`, and `c`, if `a` is equal to the sum of `c` and `b`, then the result of subtracting `b` from `a` is equal to `c`. This essentially captures the reversal relationship between addition and subtraction in the natural numbers.
More concisely: If `a` equals the sum of `b` and `c` (`a = b + c`), then `c` equals the difference between `a` and `b` (`c = a - b`).
|
Nat.eq_zero_of_add_eq_zero_left
theorem Nat.eq_zero_of_add_eq_zero_left : ∀ {n m : ℕ}, n + m = 0 → m = 0
This theorem states that for all natural numbers `n` and `m`, if the sum of `n` and `m` equals zero, then `m` must be zero. This is a property of the natural numbers, since they do not include negative numbers and thus the only way their sum could be zero is if both numbers are zero.
More concisely: If two natural numbers have a sum of zero, then each number is zero.
|
Nat.le_of_not_le
theorem Nat.le_of_not_le : ∀ {a b : ℕ}, ¬b ≤ a → a ≤ b
This theorem states that for any two natural numbers 'a' and 'b', if 'b' is not less than or equal to 'a', then 'a' must be less than or equal to 'b'. Basically, it provides a mechanism to determine the relative order of two natural numbers when one number is not less than or equal to the other.
More concisely: If a is not less than or equal to b in the natural numbers, then b is less than or equal to a.
|
Nat.le_sub_one_of_lt
theorem Nat.le_sub_one_of_lt : ∀ {a b : ℕ}, a < b → a ≤ b - 1
This theorem states that for any two natural numbers `a` and `b`, if `a` is less than `b`, then `a` is less than or equal to `b` subtracted by one. This relates to the principle that when one is subtracted from a larger natural number, the remaining number is at least as large as any natural number smaller than the original larger number.
More concisely: For all natural numbers `a` and `b`, if `a` < `b`, then `a` <= `b` - 1.
|
Nat.right_distrib
theorem Nat.right_distrib : ∀ (n m k : ℕ), (n + m) * k = n * k + m * k
This theorem, `Nat.right_distrib`, states that for any three natural numbers `n`, `m`, and `k`, the distributive property holds on the right side. In other words, multiplying the sum of `n` and `m` by `k` (`(n + m) * k`) gives the same result as multiplying `n` by `k` and `m` by `k` individually, and then adding those results (`n * k + m * k`). This is a fundamental property of arithmetic known as the right distributivity of multiplication over addition.
More concisely: For all natural numbers `n`, `m`, and `k`, `(n + m) * k` equals `(n * k + m * k)`.
|
Nat.succ_ne_self
theorem Nat.succ_ne_self : ∀ (n : ℕ), n.succ ≠ n
This theorem states that, for any natural number `n`, the successor of `n` (which is `n+1`) is not equal to `n`. In other words, adding one to any natural number does not result in the same number.
More concisely: For all natural numbers `n`, `n+1` is not equal to `n`.
|
Nat.lt_add_right
theorem Nat.lt_add_right : ∀ {a b : ℕ} (c : ℕ), a < b → a < b + c
This theorem states that for all natural numbers `a`, `b`, and `c`, if `a` is less than `b`, then `a` is also less than the sum of `b` and `c`. This corresponds to the property in ordinary arithmetic where adding a number on one side of an inequality does not affect the inequality, provided the added number is non-negative, which is always the case for natural numbers.
More concisely: For all natural numbers `a`, `b`, and `c`, if `a` < `b` then `a` < `(b + c)`.
|
Nat.eq_of_mul_eq_mul_left
theorem Nat.eq_of_mul_eq_mul_left : ∀ {m k n : ℕ}, 0 < n → n * m = n * k → m = k
This theorem states that for any three natural numbers `m`, `k`, and `n`, if `n` is greater than `0` and the product of `n` and `m` equals the product of `n` and `k`, then `m` equals `k`. In simple terms, it shows that if two products involving the same non-zero natural number are equal, then the other factors in the products are also equal. In terms of mathematical notation, if $0 < n$ and $n \cdot m = n \cdot k$, then $m = k$.
More concisely: If $0 < n$ and $n \cdot m = n \cdot k$, then $m = k$.
|
Nat.mul_comm
theorem Nat.mul_comm : ∀ (n m : ℕ), n * m = m * n
This theorem, `Nat.mul_comm`, states that for all natural numbers `n` and `m`, the multiplication of `n` and `m` is commutative. In other words, the order in which the numbers are multiplied does not change the result, so `n * m` is equal to `m * n`.
More concisely: For all natural numbers `n` and `m`, `n * m` equals `m * n`.
|
Nat.ne_of_lt'
theorem Nat.ne_of_lt' : ∀ {a b : ℕ}, a < b → b ≠ a
This theorem states that for any two natural numbers 'a' and 'b', if 'a' is less than 'b', then 'b' is not equal to 'a'. In other words, it asserts the inequality of two natural numbers when one is strictly less than the other.
More concisely: For all natural numbers a and b, if a < b then a ≠ b.
|
Nat.eq_iff_le_and_ge
theorem Nat.eq_iff_le_and_ge : ∀ {a b : ℕ}, a = b ↔ a ≤ b ∧ b ≤ a
This theorem states that for any two natural numbers `a` and `b`, `a` is equal to `b` if and only if `a` is less than or equal to `b` and `b` is less than or equal to `a`. This is a fundamental property of total orders: in such orders, `a ≤ b` and `b ≤ a` together imply that `a = b`.
More concisely: For all natural numbers `a` and `b`, `a = b` if and only if `a leq b` and `b leq a`.
|
Nat.zero_add
theorem Nat.zero_add : ∀ (n : ℕ), 0 + n = n
This theorem states that for all natural numbers 'n', the result of adding zero to 'n' is 'n' itself. In other words, it proves the identity property of addition for natural numbers, where adding zero to any natural number doesn't change its value.
More concisely: For all natural numbers n, n + 0 = n.
|
Nat.add_left_cancel
theorem Nat.add_left_cancel : ∀ {n m k : ℕ}, n + m = n + k → m = k
This theorem, `Nat.add_left_cancel`, states that for any three natural numbers `n`, `m`, and `k`, if the sum of `n` and `m` is equal to the sum of `n` and `k`, then `m` must be equal to `k`. In other words, adding the same number `n` to two different numbers `m` and `k` results in equal sums only if `m` and `k` are the same. This is a formalization of the principle of cancelation in addition for natural numbers.
More concisely: If `n`, `m`, and `k` are natural numbers such that `n + m = n + k`, then `m = k`.
|
Nat.succ_sub_succ
theorem Nat.succ_sub_succ : ∀ (n m : ℕ), n.succ - m.succ = n - m
This theorem states that for any two natural numbers `n` and `m`, the successor of `n` minus the successor of `m` is equal to `n` minus `m`. In other words, if you increment both `n` and `m` by 1, the difference between them remains the same. This is essentially a formalization of the basic arithmetic property that the difference between two numbers is invariant under the same increment to both numbers.
More concisely: For all natural numbers `n` and `m`, `(n.succ - m.succ) = (n - m)`.
|
Nat.sub_add_cancel
theorem Nat.sub_add_cancel : ∀ {n m : ℕ}, m ≤ n → n - m + m = n
This theorem states that for any two natural numbers `n` and `m`, if `m` is less than or equal to `n`, then subtracting `m` from `n` and then adding `m` back gives us `n`. This is a fundamental property of subtraction and addition in the natural numbers domain.
More concisely: For all natural numbers `n` and `m`, `n = (n - m) + m`.
|
Nat.sub_lt
theorem Nat.sub_lt : ∀ {n m : ℕ}, 0 < n → 0 < m → n - m < n
This theorem states that for any two natural numbers `n` and `m`, if `n` and `m` are both greater than 0, then the result of subtracting `m` from `n` is less than `n`. This corresponds to the intuitive understanding that subtracting a positive number from another positive number results in a smaller number.
More concisely: For all natural numbers `n` and `m` greater than 0, `n` > `m` implies `n` - `m` < `n`.
|
Nat.eq_zero_of_add_eq_zero
theorem Nat.eq_zero_of_add_eq_zero : ∀ {n m : ℕ}, n + m = 0 → n = 0 ∧ m = 0
This theorem states that for all natural numbers `n` and `m`, if the sum of `n` and `m` equals zero, then both `n` and `m` must be zero. This is because there are no natural numbers (which include zero and all positive integers) that you can add together to give a negative number, so the only way for two natural numbers to add to zero is if they are both zero.
More concisely: If two natural numbers `n` and `m` have the property that `n + m = 0`, then both `n` and `m` are equal to zero.
|
Nat.ne_of_gt
theorem Nat.ne_of_gt : ∀ {a b : ℕ}, b < a → a ≠ b
This theorem states that for any two natural numbers `a` and `b`, if `b` is less than `a`, then `a` is not equal to `b`. In other words, if one natural number is strictly greater than another, they cannot be the same number.
More concisely: For all natural numbers `a` and `b`, if `b` < `a`, then `a` ≠ `b`.
|
Nat.lt_pred_iff_succ_lt
theorem Nat.lt_pred_iff_succ_lt : ∀ {n : ℕ} {m : ℕ}, n < m.pred ↔ n.succ < m
This theorem states that for any two natural numbers `n` and `m`, `n` is less than the predecessor of `m` if and only if the successor of `n` is less than `m`. In mathematical terms, it expresses the equivalence $n < m-1 \iff n+1 < m$ for natural numbers $n$ and $m$. Here, `Nat.pred` refers to the predecessor function (subtracting 1), and `Nat.succ` refers to the successor function (adding 1).
More concisely: For natural numbers `n` and `m`, `n < m` if and only if `Nat.succ n < m`.
|
Nat.mul_assoc
theorem Nat.mul_assoc : ∀ (n m k : ℕ), n * m * k = n * (m * k)
This theorem states the associativity of multiplication for natural numbers. In other words, for any three natural numbers `n`, `m`, and `k`, the product of `n`, `m` and `k` remains the same regardless of how they are grouped. That is, `(n * m) * k` is equal to `n * (m * k)`.
More concisely: The theorem asserts that for all natural numbers `n`, `m`, and `k`, `(n * m) * k` equals `n * (m * k)`.
|
Nat.pred_succ
theorem Nat.pred_succ : ∀ (n : ℕ), n.succ.pred = n
This theorem states that for every natural number `n`, the predecessor of the successor of `n` is `n` itself. In other words, if we increment a natural number by 1 and then decrement it by 1, we get back the original number. This mirrors the intuitive understanding of the successor (or "next") and predecessor (or "previous") operations in the natural numbers.
More concisely: The successor of a natural number is the same number as the predecessor of its successor.
|
Nat.add_sub_cancel_left
theorem Nat.add_sub_cancel_left : ∀ (n m : ℕ), n + m - n = m
This theorem states that for all natural numbers 'n' and 'm', if you subtract 'n' from the sum of 'n' and 'm', you will get 'm'. In other words, this is the cancellation law of addition and subtraction for natural numbers: adding a number and then subtracting the same number leaves you with the original number.
More concisely: For all natural numbers n and m, n + m = (n + m) - n.
|
Nat.le_pred_of_lt
theorem Nat.le_pred_of_lt : ∀ {n m : ℕ}, n < m → n ≤ m.pred
This theorem states that for any two natural numbers `n` and `m`, if `n` is less than `m`, then `n` is less than or equal to the predecessor of `m`. The predecessor of a natural number is defined as the number subtracted by 1. For example, the predecessor of `m` is `m - 1`. However, for the natural number 0, its predecessor is defined as 0.
More concisely: For all natural numbers `n` and `m`, if `n` < `m`, then `n` ≤ `(m : nat)` (where `(m : nat)` denotes `m` as a natural number).
|
Nat.one_mul
theorem Nat.one_mul : ∀ (n : ℕ), 1 * n = n
This theorem states that for any natural number `n`, the product of `1` and `n` is equal to `n`. In the language of mathematics, it asserts that 1 is the multiplicative identity in the set of natural numbers, i.e., multiplying any natural number by 1 results in the same number.
More concisely: For every natural number n, 1 * n = n. (This statement asserts that the multiplicative identity 1 maps every natural number to itself in the multiplication operation.)
|
Nat.lt_succ_self
theorem Nat.lt_succ_self : ∀ (n : ℕ), n < n.succ
This theorem states that for any natural number `n`, `n` is less than the successor of `n`. In terms of ordinary mathematical notation, this is saying that ∀n ∈ ℕ, n < n + 1. Essentially, any number is always less than the next number.
More concisely: For all natural numbers `n`, `n` is less than `n + 1`.
|
Nat.not_le_of_gt
theorem Nat.not_le_of_gt : ∀ {n m : ℕ}, n > m → ¬n ≤ m
This theorem states that for any two natural numbers `n` and `m`, if `n` is greater than `m` then it is not possible for `n` to be less than or equal to `m`. This theorem embodies the intuitive concept that a larger number cannot also be smaller or equal to a smaller number.
More concisely: For all natural numbers n and m, if n > m then it is false that n <= m.
|
Nat.lt_asymm
theorem Nat.lt_asymm : ∀ {a b : ℕ}, a < b → ¬b < a
This theorem, `Nat.lt_asymm`, states that for all natural numbers `a` and `b`, if `a` is less than `b`, then it is not the case that `b` is less than `a`. Essentially, it asserts the asymmetry of the "less than" relation for natural numbers: if `a` is less than `b`, then `b` cannot be less than `a` at the same time.
More concisely: For all natural numbers `a` and `b`, if `a` is less than `b`, then `b` is not less than `a`.
|
Nat.mul_le_mul_right
theorem Nat.mul_le_mul_right : ∀ {n m : ℕ} (k : ℕ), n ≤ m → n * k ≤ m * k
This theorem states that for all natural numbers `n`, `m`, and `k`, if `n` is less than or equal to `m`, then the product of `n` and `k` is less than or equal to the product of `m` and `k`. This is a formal statement of the property that multiplication by a given natural number preserves the order of natural numbers.
More concisely: For all natural numbers `n`, `m`, and `k`, if `n ≤ m` then `n * k ≤ m * k`.
|
Nat.le_of_not_gt
theorem Nat.le_of_not_gt : ∀ {a b : ℕ}, ¬b > a → b ≤ a
This theorem states that for any two natural numbers `a` and `b`, if `b` is not greater than `a` (the statement `b > a` is not true), then `b` must be less than or equal to `a`. In mathematical terms, this theorem is saying that for all natural numbers `a` and `b`, if `¬(b > a)` then `b ≤ a`. This theorem captures one of the fundamental properties of the ordering of natural numbers.
More concisely: For all natural numbers `a` and `b`, if `b` is not greater than `a`, then `b` is less than or equal to `a` (i.e., `¬(b > a)` implies `b ≤ a`).
|
Nat.add_sub_add_right
theorem Nat.add_sub_add_right : ∀ (n k m : ℕ), n + k - (m + k) = n - m
This theorem states that for any three natural numbers `n`, `k`, and `m`, the difference between the sum of `n` and `k` and the sum of `m` and `k` equals the difference between `n` and `m`. In mathematical notation, this would be expressed as: \(n + k - (m + k) = n - m\). This theorem is a property of addition and subtraction on the natural numbers.
More concisely: For any natural numbers `n`, `k`, and `m`, `(n + k) - (m + k) = n - m`.
|
Nat.lt_of_succ_lt
theorem Nat.lt_of_succ_lt : ∀ {n m : ℕ}, n.succ < m → n < m
This theorem, `Nat.lt_of_succ_lt`, states that for any two natural numbers `n` and `m`, if the successor of `n` (which is `n+1`) is less than `m`, then `n` itself is less than `m`. This is intuitively clear, as if `n+1` is less than `m`, it is certain that `n` is also less than `m`.
More concisely: If `n+1` is less than `m`, then `n` is less than `m`.
|
Init.Data.Nat.Basic._auxLemma.3
theorem Init.Data.Nat.Basic._auxLemma.3 : ∀ (n : ℕ), (0 = n + 1) = False
This theorem, `Init.Data.Nat.Basic._auxLemma.3`, asserts that for any natural number `n`, the proposition that `n` is less than `n` is false. In other words, no natural number is less than itself.
More concisely: For all natural numbers n, n is not less than n.
|
Nat.le.dest
theorem Nat.le.dest : ∀ {n m : ℕ}, n ≤ m → ∃ k, n + k = m
This theorem, `Nat.le.dest`, states that for any two natural numbers 'n' and 'm', if 'n' is less than or equal to 'm', then there exists another natural number 'k' such that 'n' plus 'k' equals 'm'. This theorem essentially formalizes the concept that any natural number 'm' can be expressed as the sum of a smaller number 'n' and some natural number 'k'.
More concisely: For all natural numbers n and m, if n ≤ m, then there exists a natural number k such that n + k = m.
|
Nat.lt_of_succ_lt_succ
theorem Nat.lt_of_succ_lt_succ : ∀ {n m : ℕ}, n.succ < m.succ → n < m
This theorem, `Nat.lt_of_succ_lt_succ`, asserts that for any two natural numbers 'n' and 'm', if the successor of 'n' is less than the successor of 'm', then 'n' is less than 'm'. In mathematical terms, this theorem expresses the property that if `n+1 < m+1`, then it must be that `n < m`. It's a basic property of the natural numbers under the order relation.
More concisely: If `n+1 < m+1` implies `n < m` for natural numbers `n` and `m`.
|
Nat.le.intro
theorem Nat.le.intro : ∀ {n m k : ℕ}, n + k = m → n ≤ m
This theorem, `Nat.le.intro`, states that for all natural numbers `n`, `m`, and `k`, if `n + k` equals `m`, then `n` is less than or equal to `m`. It provides a method to introduce an inequality based on the properties of natural numbers, essentially stating that if you can add some natural number to `n` to reach `m`, then `n` must be less than or equal to `m`.
More concisely: If `n + k = m` for natural numbers `n`, `m`, and `k`, then `n ≤ m`.
|
Nat.add_right_comm
theorem Nat.add_right_comm : ∀ (n m k : ℕ), n + m + k = n + k + m
This theorem, `Nat.add_right_comm`, states that for any three natural numbers `n`, `m`, and `k`, the sum of `n`, `m`, and `k` remains the same even if the order of `m` and `k` is switched. In other words, it asserts the commutativity of addition on the right side, specifically that `n + m + k` is equal to `n + k + m`. This theorem is a variation of the general commutative law of addition, which states that the order of the numbers being added does not change the sum.
More concisely: For all natural numbers n, m, and k, the expression n + m + k is equal to n + k + m.
|
Nat.mul_sub_right_distrib
theorem Nat.mul_sub_right_distrib : ∀ (n m k : ℕ), (n - m) * k = n * k - m * k
This theorem, `Nat.mul_sub_right_distrib`, states that for any three natural numbers `n`, `m`, and `k`, the operation of subtracting `m` from `n` and then multiplying the result by `k` is the same as multiplying `n` and `m` separately by `k` and then subtracting the two results. In mathematical notation, this would be written as `(n - m) * k = n * k - m * k`. This theorem essentially establishes the right distributivity of multiplication over subtraction in the set of natural numbers.
More concisely: For all natural numbers `n`, `m`, and `k`, `(n - m) * k = n * k - m * k`.
|
Nat.le_lt_asymm
theorem Nat.le_lt_asymm : ∀ {a b : ℕ}, a ≤ b → ¬b < a
This theorem states that for any two natural numbers `a` and `b`, if `a` is less than or equal to `b`, then it is not possible for `b` to be less than `a`. This is a fundamental property of order in the natural numbers, ensuring that the ordering is antisymmetric: if one number is less than or equal to another, the second can't be strictly less than the first.
More concisely: For all natural numbers `a` and `b`, if `a ≤ b` then `b ≥ a`.
|
Nat.mul_le_mul_left
theorem Nat.mul_le_mul_left : ∀ {n m : ℕ} (k : ℕ), n ≤ m → k * n ≤ k * m
This theorem states that, for any natural numbers `n`, `m`, and `k`, if `n` is less than or equal to `m` (`n ≤ m`), then the product of `k` and `n` (`k * n`) is less than or equal to the product of `k` and `m` (`k * m`). In other words, multiplication by a non-negative integer preserves the order of natural numbers.
More concisely: For all natural numbers n, m, and k, if n ≤ m then k * n ≤ k * m.
|
Nat.eq_zero_of_le_zero
theorem Nat.eq_zero_of_le_zero : ∀ {n : ℕ}, n ≤ 0 → n = 0
This theorem states that for any natural number `n`, if `n` is less than or equal to zero, then `n` must be equal to zero. In other words, there is no natural number less than zero, so if a natural number is not greater than zero, it must be zero itself.
More concisely: For all natural numbers n, if n ≤ 0 then n = 0.
|
Nat.lt_succ_iff
theorem Nat.lt_succ_iff : ∀ {m n : ℕ}, m < n.succ ↔ m ≤ n
This theorem states that for any two natural numbers `m` and `n`, `m` is less than the successor of `n` if and only if `m` is less than or equal to `n`. In other words, the theorem establishes a connection between the "less than" and "less than or equal to" relations for natural numbers when considering the successor of a number.
More concisely: For all natural numbers m and n, m < (S n) if and only if m <= n, where S denotes the successor function.
|
Nat.zero_mul
theorem Nat.zero_mul : ∀ (n : ℕ), 0 * n = 0
This theorem states that for any natural number `n`, the product of `0` and `n` is `0`. In mathematical terms, this theorem formalizes the property `0*n = 0` for all natural numbers `n`, encapsulating the arithmetic rule that anything multiplied by zero equals zero.
More concisely: For all natural numbers `n`, the product of `0` and `n` is equal to `0`.
|
Nat.succ_ne_zero
theorem Nat.succ_ne_zero : ∀ (n : ℕ), n.succ ≠ 0
This theorem states that the successor of any natural number `n` is not equal to zero. In other words, if you add 1 to any natural number, you will never get zero. In mathematical terms, for every natural number `n`, `n + 1 ≠ 0`.
More concisely: For all natural numbers `n`, `n + 1 ≠ 0`.
|
Nat.lt_succ
theorem Nat.lt_succ : ∀ {m n : ℕ}, m < n.succ ↔ m ≤ n
This theorem, `Nat.lt_succ`, states that for any two natural numbers `m` and `n`, `m` is less than the successor of `n` if and only if `m` is less than or equal to `n`. In other words, it establishes an equivalence between `m` being less than `n + 1` and `m` being less than or equal to `n`. This is a fundamental property in the order theory of natural numbers.
More concisely: For all natural numbers `m` and `n`, `m` < `n` if and only if `m` <= `n`.
|
Nat.mul_lt_mul_of_pos_right
theorem Nat.mul_lt_mul_of_pos_right : ∀ {n m k : ℕ}, n < m → k > 0 → n * k < m * k
This theorem states that for any three natural numbers 'n', 'm', and 'k', if 'n' is less than 'm' and 'k' is greater than 0, then the product of 'n' and 'k' is less than the product of 'm' and 'k'. In other words, multiplication by a positive number preserves the order of natural numbers.
More concisely: For all natural numbers n, m, and k where n < m and k > 0, n * k < m * k.
|
Init.Data.Nat.Basic._auxLemma.2
theorem Init.Data.Nat.Basic._auxLemma.2 : ∀ (n : ℕ), (n + 1 = 0) = False
This theorem, `Init.Data.Nat.Basic._auxLemma.2`, asserts that for any natural number `n`, the statement that `n` is less than or equal to `n` is always true. This is a fundamental property of the ordering of natural numbers, stating that every number is always less than or equal to itself.
More concisely: For every natural number `n`, `n` is a lower bound of the relation `≤` on natural numbers, i.e., `n ≤ n` always holds.
|
Nat.le_add_left
theorem Nat.le_add_left : ∀ (n m : ℕ), n ≤ m + n
This theorem states that for any two natural numbers `n` and `m`, `n` is less than or equal to the sum of `m` and `n`. In other words, if you have any natural number `n`, adding any other natural number `m` to it either retains the value if `m` is zero or increases the value if `m` is positive.
More concisely: For all natural numbers n and m, n ≤ m + n.
|
Nat.zero_lt_one
theorem Nat.zero_lt_one : 0 < 1
This theorem states that zero is less than one in the set of natural numbers. In the language of mathematics, it is expressed as "0 < 1". This is a fundamental truth in number theory and is foundational to many other theorems and properties.
More concisely: The theorem asserts that 0 is less than 1 in the natural numbers.
|
Nat.succ_le
theorem Nat.succ_le : ∀ {n m : ℕ}, n.succ ≤ m ↔ n < m
This theorem, `Nat.succ_le`, states that for all natural numbers `n` and `m`, the successor of `n` (which is `n` plus one, represented as `Nat.succ n`) is less than or equal to `m` if and only if `n` is strictly less than `m`. In other words, adding one to a natural number `n` results in a number that is less than or equal to `m` exactly when `n` itself is less than `m`.
More concisely: For all natural numbers `n` and `m`, `Nat.succ n <= m` if and only if `n < m`.
|
Nat.mul_one
theorem Nat.mul_one : ∀ (n : ℕ), n * 1 = n
This theorem, named `Nat.mul_one`, states that for all natural numbers `n`, the product of `n` and 1 is `n` itself. In mathematical notation, this is often written as ∀n ∈ ℕ, n * 1 = n. Essentially, it formalizes the property of the multiplicative identity in natural numbers, which says that any number multiplied by 1 remains unchanged.
More concisely: For all natural numbers n, n * 1 equals n.
|
Nat.pow_succ
theorem Nat.pow_succ : ∀ (n m : ℕ), n ^ m.succ = n ^ m * n
This theorem states that for all natural numbers `n` and `m`, the power of `n` to the successor of `m` (`n` to the power of `m + 1`) is equal to the result of `n` to the power of `m` multiplied by `n`. In mathematical terms, it's saying that $n^{m + 1} = n^m * n$ for all natural numbers `n` and `m`.
More concisely: For all natural numbers `n` and `m`, `n^(m + 1)` equals `n^m * n`.
|
Nat.one_ne_zero
theorem Nat.one_ne_zero : 1 ≠ 0
This theorem, `Nat.one_ne_zero`, asserts that one is not equal to zero in the natural numbers. It's a fundamental concept in arithmetic and number theory, stating that the numbers one and zero are distinct. This is a basic property of the natural number system, and it's used often in mathematical reasoning and proofs.
More concisely: The natural number one is not equal to zero.
|
Nat.sub_zero
theorem Nat.sub_zero : ∀ (n : ℕ), n - 0 = n
This theorem, named `Nat.sub_zero`, states that for all natural numbers `n`, the result of subtracting zero from `n` is `n` itself. That is, any natural number minus zero gives the same natural number. This corresponds to the familiar arithmetic fact in mathematics that any number minus zero equals the number itself.
More concisely: For all natural numbers n, n - 0 = n.
|
Nat.le_of_lt
theorem Nat.le_of_lt : ∀ {n m : ℕ}, n < m → n ≤ m
This theorem states that for any two natural numbers `n` and `m`, if `n` is strictly less than `m` (expressed as `n < m`), then `n` is also less than or equal to `m` (expressed as `n ≤ m`). This is a fundamental property of order relations in mathematics.
More concisely: If `n` is less than `m`, then `n` is also less than or equal to `m` (`n < m` implies `n ≤ m`).
|
Nat.lt.step
theorem Nat.lt.step : ∀ {n m : ℕ}, n < m → n < m.succ
This theorem states that for all natural numbers 'n' and 'm', if 'n' is less than 'm', then 'n' is also less than the successor of 'm' (i.e., 'm' plus one). It is a fundamental property of natural numbers in order theory, asserting that if a number is less than another, it remains less than the next number in the sequence as well.
More concisely: For all natural numbers n and m, if n < m then n < m+1.
|
Nat.lt_of_not_le
theorem Nat.lt_of_not_le : ∀ {a b : ℕ}, ¬a ≤ b → b < a
This theorem, `Nat.lt_of_not_le`, states that for any two natural numbers `a` and `b`, if it is not the case that `a` is less than or equal to `b` (`¬a ≤ b`), then we can infer that `b` is strictly less than `a` (`b < a`). This is a fundamental property of ordering on the natural numbers.
More concisely: If `a` is not less than or equal to `b` (`a > b` or `a = b`), then `b` is strictly less than `a` (`b < a`).
|
Nat.mul_pos
theorem Nat.mul_pos : ∀ {n m : ℕ}, n > 0 → m > 0 → n * m > 0
This theorem, `Nat.mul_pos`, states that for any two natural numbers `n` and `m`, if both `n` and `m` are greater than zero, then their product is also greater than zero. In mathematical terms, it expresses that the product of two positive natural numbers is always positive.
More concisely: For all natural numbers `n` and `m` greater than zero, `n * m` is also greater than zero.
|
Nat.not_le
theorem Nat.not_le : ∀ {a b : ℕ}, ¬a ≤ b ↔ b < a
This theorem states that for any two natural numbers `a` and `b`, `a` is not less than or equal to `b` if and only if `b` is strictly less than `a`. In other words, it establishes an equivalence between the negation of the "less than or equal to" relation and the "strictly less than" relation.
More concisely: For natural numbers `a` and `b`, `a` is not less than or equal to `b` if and only if `b` is strictly less than `a`. Equivalently, `a < b` if and only if `a >= b` does not hold.
|
Nat.lt_or_lt_of_ne
theorem Nat.lt_or_lt_of_ne : ∀ {a b : ℕ}, a ≠ b → a < b ∨ b < a
This theorem states that for any two natural numbers `a` and `b`, if `a` is not equal to `b`, then either `a` is less than `b` or `b` is less than `a`. This is an inherent property of ordered sets, in this case, the set of natural numbers, where any two distinct elements can be ordered relative to each other.
More concisely: For all natural numbers `a` and `b`, if `a ≠ b`, then `a < b` or `b < a`.
|
Nat.mul_lt_mul_of_pos_left
theorem Nat.mul_lt_mul_of_pos_left : ∀ {n m k : ℕ}, n < m → k > 0 → k * n < k * m
This theorem states that for any three natural numbers `n`, `m`, and `k`, if `n` is less than `m` and `k` is greater than 0, then the product of `k` and `n` (i.e., `k * n`) is less than the product of `k` and `m` (i.e., `k * m`). The theorem asserts the preservation of ordering under multiplication by a positive factor in the context of natural numbers.
More concisely: For any natural numbers `n` < `m` and `k` > 0, `k * n` < `k * m`.
|
Nat.le_of_sub_eq_zero
theorem Nat.le_of_sub_eq_zero : ∀ {n m : ℕ}, n - m = 0 → n ≤ m
This theorem states that for any two natural numbers `n` and `m`, if the result of subtracting `m` from `n` equals zero, it implies that `n` is less than or equal to `m`. In mathematical terms, ∀ n, m ∈ ℕ, if n - m = 0, then n ≤ m.
More concisely: For all natural numbers `n` and `m`, if `n - m = 0` then `n <= m`.
|
Nat.lt_or_eq_of_le
theorem Nat.lt_or_eq_of_le : ∀ {n m : ℕ}, n ≤ m → n < m ∨ n = m
This theorem states that for any two natural numbers `n` and `m`, if `n` is less than or equal to `m`, then either `n` is strictly less than `m` or `n` is equal to `m`. This is a fundamental property of the ordering of natural numbers.
More concisely: For all natural numbers `n` and `m`, if `n ≤ m`, then `n < m` or `n = m`.
|
Nat.lt_le_asymm
theorem Nat.lt_le_asymm : ∀ {a b : ℕ}, a < b → ¬b ≤ a
This theorem states that for all natural numbers `a` and `b`, if `a` is less than `b`, then it is not true that `b` is less than or equal to `a`. In other words, if a natural number `a` is strictly less than another natural number `b`, then `b` cannot be less than or equal to `a`, which enforces the asymmetry of the less than relationship among natural numbers.
More concisely: For all natural numbers `a` and `b`, if `a` < `b`, then it is false that `b` <= `a`.
|
Nat.pos_pow_of_pos
theorem Nat.pos_pow_of_pos : ∀ {n : ℕ} (m : ℕ), 0 < n → 0 < n ^ m
This theorem states that for any natural number 'n' and 'm', if 'n' is greater than zero, then 'n' raised to the power 'm' is also greater than zero. In mathematical terms, it asserts that for any natural numbers 'n' and 'm', if 0 < n, then 0 < n^m. This holds true for all natural numbers since raising any positive number to a power results in a positive number.
More concisely: For any natural numbers n and m, if n > 0 then n^m > 0.
|
Nat.add_sub_cancel
theorem Nat.add_sub_cancel : ∀ (n m : ℕ), n + m - m = n
This theorem states that for any two natural numbers `n` and `m`, if you add `m` to `n` and then subtract `m`, you will get back `n`. This is a formalization of the standard arithmetic property that adding a number and then subtracting the same number leaves the original number unchanged.
More concisely: For all natural numbers `n` and `m`, `n + m = n + m + (-m)`.
|
Nat.left_distrib
theorem Nat.left_distrib : ∀ (n m k : ℕ), n * (m + k) = n * m + n * k
The theorem `Nat.left_distrib` states that for all natural numbers `n`, `m`, and `k`, the product of `n` and the sum of `m` and `k` is equal to the sum of the product of `n` and `m` and the product of `n` and `k`. This is a formalization of the distributive property of multiplication over addition, which can be written in mathematical notation as n*(m + k) = n*m + n*k.
More concisely: For all natural numbers n, m, and k, n*(m + k) = n*m + n*k. (Distributive property of multiplication over addition)
|
Nat.pow_le_pow_of_le_right
theorem Nat.pow_le_pow_of_le_right : ∀ {n : ℕ}, n > 0 → ∀ {i j : ℕ}, i ≤ j → n ^ i ≤ n ^ j
This theorem states that for any natural number `n` greater than zero, and for any two natural numbers `i` and `j` where `i` is less than or equal to `j`, the `i`-th power of `n` is less than or equal to the `j`-th power of `n`. In other words, if we have a positive natural number `n` and two natural numbers `i` and `j` with `i ≤ j`, then `n` raised to the power of `i` will always be less than or equal to `n` raised to the power of `j`.
More concisely: For all natural numbers n greater than zero and natural numbers i and j with i <= j, n^i <= n^j.
|
Nat.le_of_add_le_add_right
theorem Nat.le_of_add_le_add_right : ∀ {a b c : ℕ}, a + b ≤ c + b → a ≤ c
This theorem states that for any natural numbers `a`, `b`, and `c`, if the sum of `a` and `b` is less than or equal to the sum of `c` and `b`, then `a` is less than or equal to `c`. In mathematical terms, for all natural numbers a, b, c, if a + b ≤ c + b, then a ≤ c. This captures an important property of natural numbers with respect to addition and order relations.
More concisely: If for natural numbers a, b, and c, a + b <= c + b holds, then a <= c.
|
Nat.succ_sub_succ_eq_sub
theorem Nat.succ_sub_succ_eq_sub : ∀ (n m : ℕ), n.succ - m.succ = n - m
This theorem states that for any two natural numbers `n` and `m`, subtracting `m` from the successor of `n` (which is `n+1`) is the same as subtracting `m` from `n`. In other words, if you increment both `n` and `m` by 1, the difference between them remains unchanged.
More concisely: For all natural numbers `n` and `m`, `(n + 1) - m = n - (m - 1)`.
|
Nat.mul_left_comm
theorem Nat.mul_left_comm : ∀ (n m k : ℕ), n * (m * k) = m * (n * k)
This theorem states that for any three natural numbers `n`, `m`, and `k`, the operation of multiplication is left-commutative. In mathematical terms, this means that multiplying `n` with the product of `m` and `k` (`n * (m * k)`) is equal to multiplying `m` with the product of `n` and `k` (`m * (n * k)`).
More concisely: For all natural numbers n, m, and k, n * (m * k) = m * (n * k).
|
Nat.le_antisymm_iff
theorem Nat.le_antisymm_iff : ∀ {a b : ℕ}, a = b ↔ a ≤ b ∧ b ≤ a
This theorem states that for any two natural numbers `a` and `b`, `a` is equal to `b` if and only if `a` is less than or equal to `b` and `b` is less than or equal to `a`. In other words, if `a` is not greater than `b` and `b` is not greater than `a`, then they must be the same number. This is a formalization of the antisymmetry property of the less than or equal to relation on natural numbers.
More concisely: For all natural numbers `a` and `b`, `a = b` if and only if `a <= b` and `b <= a`.
|
Nat.sub_pos_of_lt
theorem Nat.sub_pos_of_lt : ∀ {m n : ℕ}, m < n → 0 < n - m
This theorem states that for all natural numbers `m` and `n`, if `m` is less than `n`, then the result of `n - m` is a positive natural number. Essentially, it ensures that subtracting a smaller natural number from a larger one always results in a positive value.
More concisely: For all natural numbers m and n, if m < n then n - m is a positive natural number.
|
Nat.add_sub_assoc
theorem Nat.add_sub_assoc : ∀ {m k : ℕ}, k ≤ m → ∀ (n : ℕ), n + m - k = n + (m - k)
This theorem, `Nat.add_sub_assoc`, states that for all natural numbers `m`, `k`, and `n`, if `k` is less than or equal to `m`, then adding `n` to `m` and then subtracting `k` is the same as first subtracting `k` from `m` and then adding `n`. In other words, it expresses the associative property of addition and subtraction for natural numbers when the condition `k ≤ m` is met. In terms of mathematical notation, it says that for every `m`,`k` and `n` in the set of natural numbers, if `k ≤ m` then `n + m - k = n + (m - k)`.
More concisely: For all natural numbers `m`, `k`, and `n`, if `k` is less than or equal to `m`, then `(m + n) - k` is equal to `m - k + n`.
|
Nat.add_one
theorem Nat.add_one : ∀ (n : ℕ), n + 1 = n.succ
This theorem states that for any natural number `n`, adding 1 to `n` is equivalent to obtaining the successor of `n` in the natural numbers. In other words, for any given natural number, the operation of addition by 1 yields the same result as the operation of obtaining the subsequent number.
More concisely: For any natural number `n`, `n + 1` is equal to the successor of `n`.
|