Nat.le_of_le_of_sub_le_sub_right
theorem Nat.le_of_le_of_sub_le_sub_right : ∀ {n m k : ℕ}, k ≤ m → n - k ≤ m - k → n ≤ m
This theorem, `Nat.le_of_le_of_sub_le_sub_right`, establishes a fundamental relationship between three natural numbers, `n`, `m`, and `k`. Specifically, it asserts that if `k` is less than or equal to `m` and the difference between `n` and `k` is less than or equal to the difference between `m` and `k`, then `n` is less than or equal to `m`. This is a general rule that emerges from the properties of subtraction and order relations in the set of natural numbers.
More concisely: If `k` le `m` and `n` - `k` le `m` - `k`, then `n` le `m`.
|
Nat.le_of_le_of_sub_le_sub_left
theorem Nat.le_of_le_of_sub_le_sub_left : ∀ {n k m : ℕ}, n ≤ k → k - m ≤ k - n → n ≤ m
This theorem states that for any three natural numbers `n`, `k`, and `m`, if `n` is less than or equal to `k` and the difference of `k` and `m` is less than or equal to the difference of `k` and `n`, then `n` is less than or equal to `m`. This is an alias of the theorem `Nat.le_of_sub_le_sub_left`.
More concisely: If `n` is less than or equal to `k` and the difference between `k` and `m` is less than or equal to the difference between `k` and `n`, then `n` is less than or equal to `m`.
|
Nat.lt_connex
theorem Nat.lt_connex : ∀ {a b : ℕ}, a ≠ b → a < b ∨ a > b
This theorem, named `Nat.lt_connex`, states that for any two natural numbers 'a' and 'b', if 'a' is not equal to 'b', then 'a' is either less than 'b' or greater than 'b'. It serves as an alias for another theorem `Nat.lt_or_gt_of_ne`.
More concisely: For all natural numbers 'a' and 'b', if 'a' is not equal to 'b' then 'a' is less than 'b' or 'a' is greater than 'b'.
|
Nat.succ_add_eq_succ_add
theorem Nat.succ_add_eq_succ_add : ∀ (a b : ℕ), a.succ + b = a + b.succ
This theorem, named `Nat.succ_add_eq_succ_add`, states that for any two natural numbers `a` and `b`, the successor of `a` (i.e., `a + 1` in common mathematical notation) plus `b` is equal to `a` plus the successor of `b`. In other words, adding one to the first number before summing is the same as adding one to the second number after summing. This theorem is an alias of `Nat.succ_add_eq_add_succ`.
More concisely: For all natural numbers `a` and `b`, `(a + 1) + b = a + (b + 1)`.
|
Nat.mul_lt_mul'
theorem Nat.mul_lt_mul' : ∀ {a c b d : ℕ}, a ≤ c → b < d → 0 < c → a * b < c * d
This theorem, `Nat.mul_lt_mul'`, is an alias of `Nat.mul_lt_mul_of_le_of_lt`. It asserts that for any four natural numbers `a`, `b`, `c`, and `d`, if `a` is less than or equal to `c`, `b` is strictly less than `d`, and `c` is greater than 0, then the product of `a` and `b` is strictly less than the product of `c` and `d`. In LaTeX terms, this can be written as: if $a \leq c$, $b < d$, and $c > 0$, then $a * b < c * d$.
More concisely: If $a \leq c$, $b < d$, and $c > 0$, then $a \cdot b < c \cdot d$.
|
Nat.mul_lt_mul
theorem Nat.mul_lt_mul : ∀ {a c b d : ℕ}, a < c → b ≤ d → 0 < b → a * b < c * d
The theorem `Nat.mul_lt_mul` is an alias of `Nat.mul_lt_mul_of_lt_of_le'`. It states that for any four natural numbers `a`, `b`, `c`, and `d`, if `a` is less than `c`, `b` is less than or equal to `d`, and `b` is greater than 0, then the product of `a` and `b` is less than the product of `c` and `d`. This theorem is a specific case of the more general principle that if you multiply a smaller number by a non-zero number, the result is smaller than if you multiply a larger number by the same or a greater number.
More concisely: If a < c and b > 0 then a * b < c * d.
|