Mathlib.Data.Nat.Init

Nat.default_eq_zero theorem

: default = 0

Full source

@[simp] theorem default_eq_zero : default = 0 := rfl

Default Natural Number is Zero

Informal description

The default value of the natural numbers type is $0$.

Nat.succ_pos' theorem

: 0 < succ n

Full source

lemma succ_pos' : 0 < succ n := succ_pos n

Successor of Natural Number is Positive

Informal description

For any natural number $n$, the successor of $n$ is strictly greater than zero, i.e., $0 < n + 1$.

Nat.succ_ne_succ theorem

: succ m ≠ succ n ↔ m ≠ n

Full source

lemma succ_ne_succ : succsucc m ≠ succ nsucc m ≠ succ n ↔ m ≠ n :=
  ⟨mt (congrArg Nat.succ ·), mt succ.inj⟩

Injectivity of Successor Function on Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the successor of $m$ is not equal to the successor of $n$ if and only if $m$ is not equal to $n$. In other words, $\operatorname{succ}(m) \neq \operatorname{succ}(n) \leftrightarrow m \neq n$.

Nat.succ_succ_ne_one theorem

(n : ℕ) : n.succ.succ ≠ 1

Full source

lemma succ_succ_ne_one (n : ℕ) : n.succ.succ ≠ 1 := by simp

Successor of Successor Not Equal to One

Informal description

For any natural number $n$, the successor of the successor of $n$ is not equal to $1$, i.e., $n + 2 \neq 1$.

Nat.one_lt_succ_succ theorem

(n : ℕ) : 1 < n.succ.succ

Full source

lemma one_lt_succ_succ (n : ℕ) : 1 < n.succ.succ := succ_lt_succ <| succ_pos n

Successor of successor is greater than one: $1 < n + 2$

Informal description

For any natural number $n$, the successor of the successor of $n$ is strictly greater than 1, i.e., $1 < n + 2$.

Nat.not_succ_lt_self theorem

: ¬succ n < n

Full source

lemma not_succ_lt_self : ¬ succ n < n := Nat.not_lt_of_ge n.le_succ

Successor Not Less Than Self

Informal description

For any natural number $n$, the successor of $n$ is not less than $n$ itself, i.e., $\neg (n + 1 < n)$.

Nat.succ_le_iff theorem

: succ m ≤ n ↔ m < n

Full source

lemma succ_le_iff : succsucc m ≤ n ↔ m < n := ⟨lt_of_succ_le, succ_le_of_lt⟩

Successor Inequality Equivalence: $m + 1 \leq n \leftrightarrow m < n$

Informal description

For any natural numbers $m$ and $n$, the successor of $m$ is less than or equal to $n$ if and only if $m$ is strictly less than $n$. In other words, $m + 1 \leq n \leftrightarrow m < n$.

Nat.le_succ_iff theorem

: m ≤ n.succ ↔ m ≤ n ∨ m = n.succ

Full source

lemma le_succ_iff : m ≤ n.succ ↔ m ≤ n ∨ m = n.succ := by
  refine ⟨fun hmn ↦ (Nat.lt_or_eq_of_le hmn).imp_left le_of_lt_succ, ?_⟩
  rintro (hmn | rfl)
  · exact le_succ_of_le hmn
  · exact Nat.le_refl _

Characterization of Successor Ordering in Natural Numbers

Informal description

For any natural numbers $m$ and $n$, $m \leq n + 1$ if and only if either $m \leq n$ or $m = n + 1$.

Nat.lt_iff_le_pred theorem

: ∀ {n}, 0 < n → (m < n ↔ m ≤ n - 1)

Full source

lemma lt_iff_le_pred : ∀ {n}, 0 < n → (m < n ↔ m ≤ n - 1) | _ + 1, _ => Nat.lt_succ_iff

Strict Inequality via Predecessor in Natural Numbers

Informal description

For any natural number $n > 0$, a natural number $m$ is strictly less than $n$ if and only if $m$ is less than or equal to $n - 1$.

Nat.le_of_pred_lt theorem

: ∀ {m}, pred m < n → m ≤ n

Full source

lemma le_of_pred_lt : ∀ {m}, pred m < n → m ≤ n
  | 0 => Nat.le_of_lt
  | _ + 1 => id

Predecessor Inequality Implies Original Inequality

Informal description

For any natural number $m$, if the predecessor of $m$ is less than $n$, then $m$ is less than or equal to $n$.

Nat.lt_iff_add_one_le theorem

: m < n ↔ m + 1 ≤ n

Full source

lemma lt_iff_add_one_le : m < n ↔ m + 1 ≤ n := by rw [succ_le_iff]

Strict Inequality via Successor in Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the inequality $m < n$ holds if and only if $m + 1 \leq n$.

Nat.lt_one_add_iff theorem

: m < 1 + n ↔ m ≤ n

Full source

lemma lt_one_add_iff : m < 1 + n ↔ m ≤ n := by simp only [Nat.add_comm, Nat.lt_succ_iff]

Inequality Relating Less Than and Addition of One in Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the inequality $m < 1 + n$ holds if and only if $m \leq n$.

Nat.one_add_le_iff theorem

: 1 + m ≤ n ↔ m < n

Full source

lemma one_add_le_iff : 1 + m ≤ n ↔ m < n := by simp only [Nat.add_comm, add_one_le_iff]

Inequality equivalence: $1 + m \leq n \leftrightarrow m < n$

Informal description

For any natural numbers $m$ and $n$, the inequality $1 + m \leq n$ holds if and only if $m < n$.

Nat.one_le_iff_ne_zero theorem

: 1 ≤ n ↔ n ≠ 0

Full source

lemma one_le_iff_ne_zero : 1 ≤ n ↔ n ≠ 0 := Nat.pos_iff_ne_zero

One is less than or equal to a natural number if and only if it is nonzero

Informal description

For any natural number $n$, we have $1 \leq n$ if and only if $n \neq 0$.

Nat.one_lt_iff_ne_zero_and_ne_one theorem

: ∀ {n : ℕ}, 1 < n ↔ n ≠ 0 ∧ n ≠ 1

Full source

lemma one_lt_iff_ne_zero_and_ne_one : ∀ {n : ℕ}, 1 < n ↔ n ≠ 0 ∧ n ≠ 1
  | 0 => by decide
  | 1 => by decide
  | n + 2 => by omega

Characterization of natural numbers greater than one

Informal description

For any natural number $n$, the inequality $1 < n$ holds if and only if $n$ is neither zero nor one.

Nat.le_one_iff_eq_zero_or_eq_one theorem

: ∀ {n : ℕ}, n ≤ 1 ↔ n = 0 ∨ n = 1

Full source

lemma le_one_iff_eq_zero_or_eq_one : ∀ {n : ℕ}, n ≤ 1 ↔ n = 0 ∨ n = 1 := by simp [le_succ_iff]

Natural Number at Most One is Zero or One

Informal description

For any natural number $n$, $n \leq 1$ if and only if $n = 0$ or $n = 1$.

Nat.one_le_of_lt theorem

(h : a < b) : 1 ≤ b

Full source

lemma one_le_of_lt (h : a < b) : 1 ≤ b := Nat.lt_of_le_of_lt (Nat.zero_le _) h

Lower bound of non-zero natural numbers under strict inequality

Informal description

For any natural numbers $a$ and $b$, if $a < b$ then $1 \leq b$.

Nat.min_left_comm theorem

(a b c : ℕ) : min a (min b c) = min b (min a c)

Full source

protected lemma min_left_comm (a b c : ℕ) : min a (min b c) = min b (min a c) := by
  rw [← Nat.min_assoc, ← Nat.min_assoc, b.min_comm]

Left Commutativity of Minimum Operation on Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$, the minimum of $a$ and the minimum of $b$ and $c$ is equal to the minimum of $b$ and the minimum of $a$ and $c$. In other words, $\min(a, \min(b, c)) = \min(b, \min(a, c))$.

Nat.max_left_comm theorem

(a b c : ℕ) : max a (max b c) = max b (max a c)

Full source

protected lemma max_left_comm (a b c : ℕ) : max a (max b c) = max b (max a c) := by
  rw [← Nat.max_assoc, ← Nat.max_assoc, b.max_comm]

Left Commutativity of Maximum Operation on Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$, the maximum of $a$ and the maximum of $b$ and $c$ is equal to the maximum of $b$ and the maximum of $a$ and $c$, i.e., \[ \max(a, \max(b, c)) = \max(b, \max(a, c)). \]

Nat.min_right_comm theorem

(a b c : ℕ) : min (min a b) c = min (min a c) b

Full source

protected lemma min_right_comm (a b c : ℕ) : min (min a b) c = min (min a c) b := by
  rw [Nat.min_assoc, Nat.min_assoc, b.min_comm]

Right Commutativity of Minimum Operation on Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$, the minimum of the minimum of $a$ and $b$ with $c$ is equal to the minimum of the minimum of $a$ and $c$ with $b$, i.e., \[ \min(\min(a, b), c) = \min(\min(a, c), b). \]

Nat.max_right_comm theorem

(a b c : ℕ) : max (max a b) c = max (max a c) b

Full source

protected lemma max_right_comm (a b c : ℕ) : max (max a b) c = max (max a c) b := by
  rw [Nat.max_assoc, Nat.max_assoc, b.max_comm]

Right Commutativity of Maximum Operation on Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$, the maximum of the maximum of $a$ and $b$ with $c$ is equal to the maximum of the maximum of $a$ and $c$ with $b$, i.e., \[ \max(\max(a, b), c) = \max(\max(a, c), b). \]

Nat.min_eq_zero_iff theorem

: min m n = 0 ↔ m = 0 ∨ n = 0

Full source

@[simp] lemma min_eq_zero_iff : minmin m n = 0 ↔ m = 0 ∨ n = 0 := by omega

Minimum of Natural Numbers is Zero if and Only if Either is Zero

Informal description

For any natural numbers $m$ and $n$, the minimum of $m$ and $n$ equals zero if and only if either $m$ equals zero or $n$ equals zero, i.e., \[ \min(m, n) = 0 \leftrightarrow m = 0 \lor n = 0. \]

Nat.max_eq_zero_iff theorem

: max m n = 0 ↔ m = 0 ∧ n = 0

Full source

@[simp] lemma max_eq_zero_iff : maxmax m n = 0 ↔ m = 0 ∧ n = 0 := by omega

Maximum of Two Natural Numbers is Zero if and only if Both Are Zero

Informal description

For any natural numbers $m$ and $n$, the maximum of $m$ and $n$ is zero if and only if both $m$ and $n$ are zero. In other words, $\max(m, n) = 0 \leftrightarrow m = 0 \land n = 0$.

Nat.pred_one_add theorem

(n : ℕ) : pred (1 + n) = n

Full source

lemma pred_one_add (n : ℕ) : pred (1 + n) = n := by rw [Nat.add_comm, add_one, Nat.pred_succ]

Predecessor of One Plus Natural Number

Informal description

For any natural number $n$, the predecessor of $1 + n$ equals $n$, i.e., $\mathrm{pred}(1 + n) = n$.

Nat.pred_eq_self_iff theorem

: n.pred = n ↔ n = 0

Full source

lemma pred_eq_self_iff : n.pred = n ↔ n = 0 := by cases n <;> simp [(Nat.succ_ne_self _).symm]

Predecessor Equals Number if and only if Zero

Informal description

For any natural number $n$, the predecessor of $n$ equals $n$ if and only if $n$ equals zero. In other words, $n - 1 = n \leftrightarrow n = 0$.

Nat.pred_eq_of_eq_succ theorem

(H : m = n.succ) : m.pred = n

Full source

lemma pred_eq_of_eq_succ (H : m = n.succ) : m.pred = n := by simp [H]

Predecessor of Successor Equals Original Number

Informal description

For any natural numbers $m$ and $n$, if $m$ is equal to the successor of $n$ (i.e., $m = n + 1$), then the predecessor of $m$ is equal to $n$ (i.e., $m - 1 = n$).

Nat.pred_eq_succ_iff theorem

: n - 1 = m + 1 ↔ n = m + 2

Full source

@[simp] lemma pred_eq_succ_iff : n - 1 = m + 1 ↔ n = m + 2 := by
  cases n <;> constructor <;> rintro ⟨⟩ <;> rfl

Predecessor-Successor Equality: $n - 1 = m + 1 \leftrightarrow n = m + 2$

Informal description

For natural numbers $n$ and $m$, the predecessor of $n$ equals the successor of $m$ if and only if $n$ equals $m + 2$. In other words, $n - 1 = m + 1 \leftrightarrow n = m + 2$.

Nat.forall_lt_succ theorem

: (∀ m < n + 1, p m) ↔ (∀ m < n, p m) ∧ p n

Full source

lemma forall_lt_succ : (∀ m < n + 1, p m) ↔ (∀ m < n, p m) ∧ p n := by
  simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq, or_comm, forall_eq_or_imp, and_comm]

Universal Property for Numbers Less Than Successor: $(\forall m < n+1, p(m)) \leftrightarrow (\forall m < n, p(m)) \land p(n)$

Informal description

For any natural number $n$ and property $p$, the statement that $p(m)$ holds for all $m < n + 1$ is equivalent to the conjunction of $p(m)$ holding for all $m < n$ and $p(n)$ holding.

Nat.exists_lt_succ theorem

: (∃ m < n + 1, p m) ↔ (∃ m < n, p m) ∨ p n

Full source

lemma exists_lt_succ : (∃ m < n + 1, p m) ↔ (∃ m < n, p m) ∨ p n := by
  classical
  rw [← Decidable.not_iff_not]
  simpa [not_exists, not_or] using forall_lt_succ

Existential Property for Numbers Less Than Successor: $(\exists m < n+1, p(m)) \leftrightarrow (\exists m < n, p(m)) \lor p(n)$

Informal description

For any natural number $n$ and property $p$, there exists an $m < n + 1$ satisfying $p(m)$ if and only if either there exists an $m < n$ satisfying $p(m)$ or $p(n)$ holds.

Nat.two_lt_of_ne theorem

: ∀ {n}, n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n

Full source

lemma two_lt_of_ne : ∀ {n}, n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n
  | 0, h, _, _ => (h rfl).elim
  | 1, _, h, _ => (h rfl).elim
  | 2, _, _, h => (h rfl).elim
  | n + 3, _, _, _ => le_add_left 3 n

Natural numbers greater than two satisfy $2 < n$

Informal description

For any natural number $n$, if $n$ is not equal to 0, 1, or 2, then $2 < n$.

Nat.add_succ_sub_one theorem

(m n : ℕ) : m + succ n - 1 = m + n

Full source

@[simp] lemma add_succ_sub_one (m n : ℕ) : m + succ n - 1 = m + n := rfl

Simplification of $(m + (n + 1)) - 1$ to $m + n$ in natural numbers

Informal description

For any natural numbers $m$ and $n$, we have $(m + (n + 1)) - 1 = m + n$.

Nat.succ_add_sub_one theorem

(n m : ℕ) : succ m + n - 1 = m + n

Full source

@[simp]
lemma succ_add_sub_one (n m : ℕ) : succ m + n - 1 = m + n := by rw [succ_add, Nat.add_one_sub_one]

Successor Addition and Subtraction Identity: $(\mathrm{succ}\,m) + n - 1 = m + n$

Informal description

For any natural numbers $n$ and $m$, the expression $(\mathrm{succ}\,m) + n - 1$ equals $m + n$.

Nat.pred_sub theorem

(n m : ℕ) : pred n - m = pred (n - m)

Full source

lemma pred_sub (n m : ℕ) : pred n - m = pred (n - m) := by
  rw [← Nat.sub_one, Nat.sub_sub, one_add, sub_succ]

Predecessor and Subtraction Commute on Natural Numbers

Informal description

For any natural numbers $n$ and $m$, the predecessor of $n$ minus $m$ is equal to the predecessor of $(n - m)$. That is, $\mathrm{pred}(n) - m = \mathrm{pred}(n - m)$.

Nat.self_add_sub_one theorem

: ∀ n, n + (n - 1) = 2 * n - 1

Full source

lemma self_add_sub_one : ∀ n, n + (n - 1) = 2 * n - 1
  | 0 => rfl
  | n + 1 => by rw [Nat.two_mul]; exact (add_succ_sub_one (Nat.succ _) _).symm

Sum of Number and Its Predecessor Equals Twice Number Minus One

Informal description

For any natural number $n$, the sum of $n$ and $(n - 1)$ equals $2n - 1$, i.e., $n + (n - 1) = 2n - 1$.

Nat.sub_one_add_self theorem

(n : ℕ) : (n - 1) + n = 2 * n - 1

Full source

lemma sub_one_add_self (n : ℕ) : (n - 1) + n = 2 * n - 1 := Nat.add_comm _ n ▸ self_add_sub_one n

Sum of Predecessor and Number Equals Twice Number Minus One

Informal description

For any natural number $n$, the sum of $(n - 1)$ and $n$ equals $2n - 1$, i.e., $(n - 1) + n = 2n - 1$.

Nat.self_add_pred theorem

(n : ℕ) : n + pred n = (2 * n).pred

Full source

lemma self_add_pred (n : ℕ) : n + pred n = (2 * n).pred := self_add_sub_one n

Sum of Number and Its Predecessor Equals Predecessor of Twice Number

Informal description

For any natural number $n$, the sum of $n$ and its predecessor equals the predecessor of $2n$, i.e., $n + \operatorname{pred}(n) = \operatorname{pred}(2n)$.

Nat.pred_add_self theorem

(n : ℕ) : pred n + n = (2 * n).pred

Full source

lemma pred_add_self (n : ℕ) : pred n + n = (2 * n).pred := sub_one_add_self n

Predecessor Sum Identity: $\operatorname{pred}(n) + n = \operatorname{pred}(2n)$

Informal description

For any natural number $n$, the sum of the predecessor of $n$ and $n$ itself equals the predecessor of twice $n$, i.e., $\operatorname{pred}(n) + n = \operatorname{pred}(2n)$.

Nat.pred_le_iff theorem

: pred m ≤ n ↔ m ≤ succ n

Full source

lemma pred_le_iff : predpred m ≤ n ↔ m ≤ succ n :=
  ⟨le_succ_of_pred_le, by
    cases m
    · exact fun _ ↦ zero_le n
    · exact le_of_succ_le_succ⟩

Predecessor-Leq-Successor Equivalence for Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the predecessor of $m$ is less than or equal to $n$ if and only if $m$ is less than or equal to the successor of $n$. In other words: $$\operatorname{pred}(m) \leq n \leftrightarrow m \leq \operatorname{succ}(n)$$

Nat.lt_of_lt_pred theorem

(h : m < n - 1) : m < n

Full source

lemma lt_of_lt_pred (h : m < n - 1) : m < n := by omega

Strict Inequality Preservation under Predecessor Subtraction

Informal description

For any natural numbers $m$ and $n$, if $m < n - 1$, then $m < n$.

Nat.le_add_pred_of_pos theorem

(a : ℕ) (hb : b ≠ 0) : a ≤ b + (a - 1)

Full source

lemma le_add_pred_of_pos (a : ℕ) (hb : b ≠ 0) : a ≤ b + (a - 1) := by omega

Inequality for Addition with Predecessor in Natural Numbers

Informal description

For any natural numbers $a$ and $b$ with $b \neq 0$, we have $a \leq b + (a - 1)$.

Nat.add_eq_left theorem

: a + b = a ↔ b = 0

Full source

@[simp high] protected lemma add_eq_left : a + b = a ↔ b = 0 := by omega

Sum Equals First Addend if and only if Second Addend is Zero

Informal description

For natural numbers $a$ and $b$, the sum $a + b$ equals $a$ if and only if $b = 0$.

Nat.add_eq_right theorem

: a + b = b ↔ a = 0

Full source

@[simp high] protected lemma add_eq_right : a + b = b ↔ a = 0 := by omega

Sum Equals Second Addend iff First Addend is Zero

Informal description

For any natural numbers $a$ and $b$, the sum $a + b$ equals $b$ if and only if $a = 0$.

Nat.two_le_iff theorem

: ∀ n, 2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1

Full source

lemma two_le_iff : ∀ n, 2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1
  | 0 => by simp
  | 1 => by simp
  | n + 2 => by simp

Characterization of Natural Numbers Greater Than or Equal to Two

Informal description

For any natural number $n$, the inequality $2 \leq n$ holds if and only if $n$ is neither zero nor one, i.e., $n \neq 0$ and $n \neq 1$.

Nat.add_eq_max_iff theorem

: m + n = max m n ↔ m = 0 ∨ n = 0

Full source

lemma add_eq_max_iff : m + n = max m n ↔ m = 0 ∨ n = 0 := by omega

Sum Equals Maximum iff One Term is Zero

Informal description

For any natural numbers $m$ and $n$, the sum $m + n$ equals the maximum of $m$ and $n$ if and only if either $m = 0$ or $n = 0$.

Nat.add_eq_min_iff theorem

: m + n = min m n ↔ m = 0 ∧ n = 0

Full source

lemma add_eq_min_iff : m + n = min m n ↔ m = 0 ∧ n = 0 := by omega

Sum Equals Minimum if and only if Both Zero

Informal description

For any natural numbers $m$ and $n$, the sum $m + n$ equals the minimum of $m$ and $n$ if and only if both $m$ and $n$ are zero. In other words, $m + n = \min(m, n) \leftrightarrow m = 0 \land n = 0$.

Nat.add_eq_zero theorem

: m + n = 0 ↔ m = 0 ∧ n = 0

Full source

@[simp high] protected lemma add_eq_zero : m + n = 0 ↔ m = 0 ∧ n = 0 := by omega

Sum of Natural Numbers is Zero iff Both Zero

Informal description

For any natural numbers $m$ and $n$, the sum $m + n$ equals zero if and only if both $m = 0$ and $n = 0$.

Nat.add_pos_iff_pos_or_pos theorem

: 0 < m + n ↔ 0 < m ∨ 0 < n

Full source

lemma add_pos_iff_pos_or_pos : 0 < m + n ↔ 0 < m ∨ 0 < n := by omega

Positivity of Sum in Natural Numbers: $0 < m + n \leftrightarrow 0 < m \lor 0 < n$

Informal description

For any natural numbers $m$ and $n$, the sum $m + n$ is positive if and only if at least one of $m$ or $n$ is positive. In other words, $0 < m + n \leftrightarrow 0 < m \lor 0 < n$.

Nat.add_eq_one_iff theorem

: m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0

Full source

lemma add_eq_one_iff : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 := by omega

Sum of Two Natural Numbers Equals One if and only if One is Zero and the Other is One

Informal description

For natural numbers $m$ and $n$, the sum $m + n$ equals $1$ if and only if either $m = 0$ and $n = 1$, or $m = 1$ and $n = 0$.

Nat.add_eq_two_iff theorem

: m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0

Full source

lemma add_eq_two_iff : m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0 := by
  omega

Characterization of Natural Number Pairs Summing to 2

Informal description

For any natural numbers $m$ and $n$, the sum $m + n$ equals 2 if and only if one of the following holds: 1. $m = 0$ and $n = 2$, or 2. $m = 1$ and $n = 1$, or 3. $m = 2$ and $n = 0$.

Nat.add_eq_three_iff theorem

: m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0

Full source

lemma add_eq_three_iff :
    m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0 := by
  omega

Characterization of Natural Number Pairs Summing to 3

Informal description

For any natural numbers $m$ and $n$, the sum $m + n$ equals $3$ if and only if one of the following holds: 1. $m = 0$ and $n = 3$, or 2. $m = 1$ and $n = 2$, or 3. $m = 2$ and $n = 1$, or 4. $m = 3$ and $n = 0$.

Nat.le_add_one_iff theorem

: m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

Full source

lemma le_add_one_iff : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1 := by omega

Characterization of $m \leq n + 1$ in Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the inequality $m \leq n + 1$ holds if and only if either $m \leq n$ or $m = n + 1$.

Nat.le_and_le_add_one_iff theorem

: n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1

Full source

lemma le_and_le_add_one_iff : n ≤ m ∧ m ≤ n + 1n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1 := by omega

Characterization of Adjacent Natural Numbers via Inequalities

Informal description

For natural numbers $n$ and $m$, the inequalities $n \leq m$ and $m \leq n + 1$ hold if and only if either $m = n$ or $m = n + 1$.

Nat.add_succ_lt_add theorem

(hab : a < b) (hcd : c < d) : a + c + 1 < b + d

Full source

lemma add_succ_lt_add (hab : a < b) (hcd : c < d) : a + c + 1 < b + d := by omega

Strict Inequality Preservation under Addition with Successor: $a + c + 1 < b + d$

Informal description

For any natural numbers $a, b, c, d$ such that $a < b$ and $c < d$, it holds that $a + c + 1 < b + d$.

Nat.le_or_le_of_add_eq_add_pred theorem

(h : a + c = b + d - 1) : b ≤ a ∨ d ≤ c

Full source

theorem le_or_le_of_add_eq_add_pred (h : a + c = b + d - 1) : b ≤ a ∨ d ≤ c := by omega

Disjunction of Inequalities from Additive Predicate Equation

Informal description

For any natural numbers $a, b, c, d$, if $a + c = b + d - 1$, then either $b \leq a$ or $d \leq c$.

Nat.sub_succ' theorem

(m n : ℕ) : m - n.succ = m - n - 1

Full source

/-- A version of `Nat.sub_succ` in the form `_ - 1` instead of `Nat.pred _`. -/
lemma sub_succ' (m n : ℕ) : m - n.succ = m - n - 1 := rfl

Subtraction of Successor: $m - (n + 1) = (m - n) - 1$

Informal description

For any natural numbers $m$ and $n$, the subtraction $m - (n + 1)$ is equal to $(m - n) - 1$.

Nat.sub_eq_of_eq_add' theorem

(h : a = b + c) : a - b = c

Full source

protected lemma sub_eq_of_eq_add' (h : a = b + c) : a - b = c := by omega

Subtraction of Natural Numbers from Sum

Informal description

For any natural numbers $a, b, c$, if $a = b + c$, then $a - b = c$.

Nat.lt_sub_iff_add_lt theorem

: a < c - b ↔ a + b < c

Full source

protected lemma lt_sub_iff_add_lt : a < c - b ↔ a + b < c := ⟨add_lt_of_lt_sub, lt_sub_of_add_lt⟩

Subtraction Inequality Equivalence: $a < c - b ↔ a + b < c$

Informal description

For any natural numbers $a$, $b$, and $c$, the inequality $a < c - b$ holds if and only if $a + b < c$.

Nat.lt_sub_iff_add_lt' theorem

: a < c - b ↔ b + a < c

Full source

protected lemma lt_sub_iff_add_lt' : a < c - b ↔ b + a < c := by omega

Inequality relating subtraction and addition: $a < c - b \leftrightarrow b + a < c$

Informal description

For any natural numbers $a$, $b$, and $c$, the inequality $a < c - b$ holds if and only if $b + a < c$.

Nat.sub_lt_iff_lt_add theorem

(hba : b ≤ a) : a - b < c ↔ a < c + b

Full source

protected lemma sub_lt_iff_lt_add (hba : b ≤ a) : a - b < c ↔ a < c + b := by omega

Subtraction Inequality: $a - b < c \leftrightarrow a < c + b$ under $b \leq a$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $b \leq a$, the inequality $a - b < c$ holds if and only if $a < c + b$.

Nat.sub_lt_iff_lt_add' theorem

(hba : b ≤ a) : a - b < c ↔ a < b + c

Full source

protected lemma sub_lt_iff_lt_add' (hba : b ≤ a) : a - b < c ↔ a < b + c := by omega

Subtraction Inequality: $a - b < c \leftrightarrow a < b + c$ under $b \leq a$

Informal description

For natural numbers $a$, $b$, and $c$ with $b \leq a$, the inequality $a - b < c$ holds if and only if $a < b + c$.

Nat.sub_sub_sub_cancel_right theorem

(h : c ≤ b) : a - c - (b - c) = a - b

Full source

protected lemma sub_sub_sub_cancel_right (h : c ≤ b) : a - c - (b - c) = a - b := by omega

Subtraction Cancellation: $(a - c) - (b - c) = a - b$ for $c \leq b$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $c \leq b$, the following equality holds: $$(a - c) - (b - c) = a - b.$$

Nat.add_sub_sub_cancel theorem

(h : c ≤ a) : a + b - (a - c) = b + c

Full source

protected lemma add_sub_sub_cancel (h : c ≤ a) : a + b - (a - c) = b + c := by omega

Subtraction-Add Cancellation: $(a + b) - (a - c) = b + c$ for $c \leq a$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $c \leq a$, the following equality holds: $$(a + b) - (a - c) = b + c.$$

Nat.sub_add_sub_cancel theorem

(hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c

Full source

protected lemma sub_add_sub_cancel (hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c := by omega

Subtraction-Additive Cancellation: $(a - b) + (b - c) = a - c$ for $b \leq a$ and $c \leq b$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $b \leq a$ and $c \leq b$, the following equality holds: $$(a - b) + (b - c) = a - c.$$

Nat.lt_pred_iff theorem

: a < pred b ↔ succ a < b

Full source

lemma lt_pred_iff : a < pred b ↔ succ a < b := Nat.lt_sub_iff_add_lt (b := 1)

Predecessor-Successor Inequality: $a < b-1 ↔ a+1 < b$

Informal description

For any natural numbers $a$ and $b$, the inequality $a < \text{pred}(b)$ holds if and only if $\text{succ}(a) < b$, where $\text{pred}(b)$ is the predecessor of $b$ (equal to $b-1$ when $b > 0$) and $\text{succ}(a)$ is the successor of $a$ (equal to $a+1$).

Nat.sub_lt_sub_iff_right theorem

(h : c ≤ a) : a - c < b - c ↔ a < b

Full source

protected lemma sub_lt_sub_iff_right (h : c ≤ a) : a - c < b - c ↔ a < b := by omega

Subtraction Preserves Strict Inequality in Natural Numbers

Informal description

For natural numbers $a$, $b$, and $c$ such that $c \leq a$, the inequality $a - c < b - c$ holds if and only if $a < b$.

Nat.mul_def theorem

: Nat.mul m n = m * n

Full source

@[simp] lemma mul_def : Nat.mul m n = m * n := rfl

Definition of Natural Number Multiplication: `Nat.mul m n = m × n`

Informal description

The multiplication of two natural numbers $m$ and $n$ defined via the `Nat.mul` function is equal to the product $m \times n$ (where $\times$ denotes standard multiplication of natural numbers).

Nat.zero_eq_mul theorem

: 0 = m * n ↔ m = 0 ∨ n = 0

Full source

protected lemma zero_eq_mul : 0 = m * n ↔ m = 0 ∨ n = 0 := by rw [eq_comm, Nat.mul_eq_zero]

Zero Product Property for Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the product $m \cdot n$ equals zero if and only if either $m$ equals zero or $n$ equals zero, i.e., $0 = m \cdot n \leftrightarrow m = 0 \lor n = 0$.

Nat.two_mul_ne_two_mul_add_one theorem

: 2 * n ≠ 2 * m + 1

Full source

lemma two_mul_ne_two_mul_add_one : 2 * n ≠ 2 * m + 1 :=
  mt (congrArg (· % 2))
    (by rw [Nat.add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt] <;> simp)

Twice a Natural Number Cannot Equal Twice Another Plus One

Informal description

For any natural numbers $n$ and $m$, twice $n$ is not equal to twice $m$ plus one, i.e., $2n \neq 2m + 1$.

Nat.mul_left_inj theorem

(ha : a ≠ 0) : b * a = c * a ↔ b = c

Full source

protected lemma mul_left_inj (ha : a ≠ 0) : b * a = c * a ↔ b = c :=
  Nat.mul_right_cancel_iff (Nat.pos_iff_ne_zero.2 ha)

Left Cancellation Law for Multiplication of Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$, if $a \neq 0$, then $b \cdot a = c \cdot a$ if and only if $b = c$.

Nat.mul_right_inj theorem

(ha : a ≠ 0) : a * b = a * c ↔ b = c

Full source

protected lemma mul_right_inj (ha : a ≠ 0) : a * b = a * c ↔ b = c :=
  Nat.mul_left_cancel_iff (Nat.pos_iff_ne_zero.2 ha)

Right Cancellation Law for Multiplication of Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$, if $a \neq 0$, then $a \cdot b = a \cdot c$ if and only if $b = c$.

Nat.mul_ne_mul_left theorem

(ha : a ≠ 0) : b * a ≠ c * a ↔ b ≠ c

Full source

protected lemma mul_ne_mul_left (ha : a ≠ 0) : b * a ≠ c * ab * a ≠ c * a ↔ b ≠ c :=
  not_congr (Nat.mul_left_inj ha)

Non-equality under Left Multiplication by Nonzero Natural Numbers: $b \cdot a \neq c \cdot a \leftrightarrow b \neq c$

Informal description

For any natural numbers $a$, $b$, and $c$ with $a \neq 0$, the product $b \cdot a$ is not equal to $c \cdot a$ if and only if $b$ is not equal to $c$.

Nat.mul_ne_mul_right theorem

(ha : a ≠ 0) : a * b ≠ a * c ↔ b ≠ c

Full source

protected lemma mul_ne_mul_right (ha : a ≠ 0) : a * b ≠ a * ca * b ≠ a * c ↔ b ≠ c :=
  not_congr (Nat.mul_right_inj ha)

Right Multiplication Preserves Inequality in Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$ with $a \neq 0$, the inequality $a \cdot b \neq a \cdot c$ holds if and only if $b \neq c$.

Nat.mul_eq_left theorem

(ha : a ≠ 0) : a * b = a ↔ b = 1

Full source

lemma mul_eq_left (ha : a ≠ 0) : a * b = a ↔ b = 1 := by simpa using Nat.mul_right_inj ha (c := 1)

Left Multiplication Identity Condition for Natural Numbers

Informal description

For any natural numbers $a$ and $b$ with $a \neq 0$, the product $a \cdot b$ equals $a$ if and only if $b = 1$.

Nat.mul_eq_right theorem

(hb : b ≠ 0) : a * b = b ↔ a = 1

Full source

lemma mul_eq_right (hb : b ≠ 0) : a * b = b ↔ a = 1 := by simpa using Nat.mul_left_inj hb (c := 1)

Right Multiplication Identity for Natural Numbers: $a \cdot b = b \leftrightarrow a = 1$

Informal description

For any natural numbers $a$ and $b$ with $b \neq 0$, the equality $a \cdot b = b$ holds if and only if $a = 1$.

Nat.mul_right_eq_self_iff theorem

(ha : 0 < a) : a * b = a ↔ b = 1

Full source

lemma mul_right_eq_self_iff (ha : 0 < a) : a * b = a ↔ b = 1 := mul_eq_left <| ne_of_gt ha

Right Multiplication Identity Condition for Positive Natural Numbers: $a \cdot b = a \leftrightarrow b = 1$

Informal description

For any natural numbers $a$ and $b$ with $a > 0$, the product $a \cdot b$ equals $a$ if and only if $b = 1$.

Nat.mul_left_eq_self_iff theorem

(hb : 0 < b) : a * b = b ↔ a = 1

Full source

lemma mul_left_eq_self_iff (hb : 0 < b) : a * b = b ↔ a = 1 := mul_eq_right <| ne_of_gt hb

Left Multiplication Identity for Positive Natural Numbers: $a \cdot b = b \leftrightarrow a = 1$

Informal description

For any natural numbers $a$ and $b$ with $b > 0$, the equality $a \cdot b = b$ holds if and only if $a = 1$.

Nat.one_lt_mul_iff theorem

: 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)

Full source

/-- The product of two natural numbers is greater than 1 if and only if
  at least one of them is greater than 1 and both are positive. -/
lemma one_lt_mul_iff : 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n) := by
  constructor <;> intro h
  · by_contra h'
    simp only [Nat.le_zero, Decidable.not_and_iff_not_or_not, not_or, Nat.not_lt] at h'
    obtain rfl | rfl | h' := h'
    · simp at h
    · simp at h
    · exact Nat.not_lt_of_le (Nat.mul_le_mul h'.1 h'.2) h
  · obtain hm | hn := h.2.2
    · exact Nat.mul_lt_mul_of_lt_of_le' hm h.2.1 Nat.zero_lt_one
    · exact Nat.mul_lt_mul_of_le_of_lt h.1 hn h.1

Product Greater Than One Criterion for Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the product $m \cdot n$ is greater than 1 if and only if both $m$ and $n$ are positive, and at least one of them is greater than 1. That is: $$1 < m \cdot n \leftrightarrow 0 < m \land 0 < n \land (1 < m \lor 1 < n)$$

Nat.lt_mul_iff_one_lt_left theorem

(hb : 0 < b) : b < a * b ↔ 1 < a

Full source

@[simp] protected lemma lt_mul_iff_one_lt_left (hb : 0 < b) : b < a * b ↔ 1 < a := by
  simpa using Nat.mul_lt_mul_right (b := 1) hb

Inequality Relating Multiplication and One in Natural Numbers (Left Version)

Informal description

For any positive natural numbers $a$ and $b$, the inequality $b < a \cdot b$ holds if and only if $1 < a$.

Nat.lt_mul_iff_one_lt_right theorem

(ha : 0 < a) : a < a * b ↔ 1 < b

Full source

@[simp] protected lemma lt_mul_iff_one_lt_right (ha : 0 < a) : a < a * b ↔ 1 < b := by
  simpa using Nat.mul_lt_mul_left (b := 1) ha

Inequality Relating Multiplication and One in Natural Numbers

Informal description

For any positive natural numbers $a$ and $b$, the inequality $a < a \cdot b$ holds if and only if $1 < b$.

Nat.succ_mul_pos theorem

(m : ℕ) (hn : 0 < n) : 0 < succ m * n

Full source

lemma succ_mul_pos (m : ℕ) (hn : 0 < n) : 0 < succ m * n := Nat.mul_pos m.succ_pos hn

Positivity of Successor Multiplication in Natural Numbers

Informal description

For any natural numbers $m$ and $n$ such that $0 < n$, it holds that $0 < (m + 1) \times n$.

Nat.mul_self_le_mul_self theorem

(h : m ≤ n) : m * m ≤ n * n

Full source

lemma mul_self_le_mul_self (h : m ≤ n) : m * m ≤ n * n := Nat.mul_le_mul h h

Square Preserves Non-Strict Inequality in Natural Numbers

Informal description

For any natural numbers $m$ and $n$, if $m \leq n$, then $m^2 \leq n^2$.

Nat.mul_lt_mul'' theorem

(hac : a < c) (hbd : b < d) : a * b < c * d

Full source

lemma mul_lt_mul'' (hac : a < c) (hbd : b < d) : a * b < c * d :=
  Nat.mul_lt_mul_of_lt_of_le hac (Nat.le_of_lt hbd) <| by omega

Multiplication Preserves Strict Inequality in Natural Numbers

Informal description

For any natural numbers $a, b, c, d$, if $a < c$ and $b < d$, then $a \times b < c \times d$.

Nat.lt_iff_lt_of_mul_eq_mul theorem

(ha : a ≠ 0) (hbd : a = b * d) (hce : a = c * e) : c < b ↔ d < e

Full source

protected lemma lt_iff_lt_of_mul_eq_mul (ha : a ≠ 0) (hbd : a = b * d) (hce : a = c * e) :
    c < b ↔ d < e where
  mp hcb := Nat.lt_of_not_le fun hed ↦ Nat.not_lt_of_le (Nat.le_of_eq <| hbd.symm.trans hce) <|
    Nat.mul_lt_mul_of_lt_of_le hcb hed <| by simp [hbd, Nat.mul_eq_zero] at ha; omega
  mpr hde := Nat.lt_of_not_le fun hbc ↦ Nat.not_lt_of_le (Nat.le_of_eq <| hce.symm.trans hbd) <|
    Nat.mul_lt_mul_of_le_of_lt hbc hde <| by simp [hce, Nat.mul_eq_zero] at ha; omega

Comparison of Factors via Product Equality in Natural Numbers

Informal description

For any nonzero natural number $a$ and natural numbers $b, c, d, e$ such that $a = b \times d$ and $a = c \times e$, the inequality $c < b$ holds if and only if $d < e$.

Nat.mul_self_lt_mul_self theorem

(h : m < n) : m * m < n * n

Full source

lemma mul_self_lt_mul_self (h : m < n) : m * m < n * n := mul_lt_mul'' h h

Square Preserves Strict Inequality in Natural Numbers

Informal description

For any natural numbers $m$ and $n$ such that $m < n$, it holds that $m^2 < n^2$.

Nat.mul_self_le_mul_self_iff theorem

: m * m ≤ n * n ↔ m ≤ n

Full source

lemma mul_self_le_mul_self_iff : m * m ≤ n * n ↔ m ≤ n :=
  ⟨fun h => Nat.le_of_not_lt fun h' => Nat.not_le_of_gt (mul_self_lt_mul_self h') h,
   mul_self_le_mul_self⟩

Square Preserves Non-Strict Order in Natural Numbers: $m^2 \leq n^2 \leftrightarrow m \leq n$

Informal description

For any natural numbers $m$ and $n$, the inequality $m^2 \leq n^2$ holds if and only if $m \leq n$.

Nat.mul_self_lt_mul_self_iff theorem

: m * m < n * n ↔ m < n

Full source

lemma mul_self_lt_mul_self_iff : m * m < n * n ↔ m < n := by
  simp only [← Nat.not_le, mul_self_le_mul_self_iff]

Square Preserves Strict Order in Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the square of $m$ is strictly less than the square of $n$ if and only if $m$ is strictly less than $n$. In other words, $m^2 < n^2 \leftrightarrow m < n$.

Nat.le_mul_self theorem

: ∀ n : ℕ, n ≤ n * n

Full source

lemma le_mul_self : ∀ n : ℕ, n ≤ n * n
  | 0 => Nat.le_refl _
  | n + 1 => by simp [Nat.mul_add]

Natural number is less than or equal to its square

Informal description

For any natural number $n$, it holds that $n \leq n \times n$.

Nat.mul_self_inj theorem

: m * m = n * n ↔ m = n

Full source

lemma mul_self_inj : m * m = n * n ↔ m = n := by
  simp [Nat.le_antisymm_iff, mul_self_le_mul_self_iff]

Square Function is Injective on Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the equality $m^2 = n^2$ holds if and only if $m = n$.

Nat.lt_mul_self_iff theorem

: ∀ {n : ℕ}, n < n * n ↔ 1 < n

Full source

@[simp] lemma lt_mul_self_iff : ∀ {n : ℕ}, n < n * n ↔ 1 < n
  | 0 => by simp
  | n + 1 => Nat.lt_mul_iff_one_lt_left n.succ_pos

Square Inequality for Natural Numbers: $n < n^2 \leftrightarrow 1 < n$

Informal description

For any natural number $n$, the inequality $n < n^2$ holds if and only if $1 < n$.

Nat.add_sub_one_le_mul theorem

(ha : a ≠ 0) (hb : b ≠ 0) : a + b - 1 ≤ a * b

Full source

lemma add_sub_one_le_mul (ha : a ≠ 0) (hb : b ≠ 0) : a + b - 1 ≤ a * b := by
  cases a
  · cases ha rfl
  · rw [succ_add, Nat.add_one_sub_one, succ_mul]
    exact Nat.add_le_add_right (Nat.le_mul_of_pos_right _ <| Nat.pos_iff_ne_zero.2 hb) _

Inequality Relating Sum and Product of Nonzero Natural Numbers

Informal description

For any nonzero natural numbers $a$ and $b$, the inequality $a + b - 1 \leq a \times b$ holds.

Nat.add_le_mul theorem

{a : ℕ} (ha : 2 ≤ a) : ∀ {b : ℕ} (_ : 2 ≤ b), a + b ≤ a * b

Full source

protected lemma add_le_mul {a : ℕ} (ha : 2 ≤ a) : ∀ {b : ℕ} (_ : 2 ≤ b), a + b ≤ a * b
  | 2, _ => by omega
  | b + 3, _ => by have := Nat.add_le_mul ha (Nat.le_add_left _ b); rw [mul_succ]; omega

Sum of natural numbers at least 2 is bounded by their product

Informal description

For any natural numbers $a$ and $b$ such that $2 \leq a$ and $2 \leq b$, the sum $a + b$ is less than or equal to the product $a \times b$.

Nat.le_div_two_iff_mul_two_le theorem

{n m : ℕ} : m ≤ n / 2 ↔ (m : ℤ) * 2 ≤ n

Full source

lemma le_div_two_iff_mul_two_le {n m : ℕ} : m ≤ n / 2 ↔ (m : ℤ) * 2 ≤ n := by
  rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.ofNat_mul, Int.ofNat_two]

Natural Number Division by Two Inequality: $m \leq n/2 \leftrightarrow 2m \leq n$

Informal description

For any natural numbers $n$ and $m$, the inequality $m \leq n / 2$ holds if and only if $2m \leq n$ (where $m$ is considered as an integer in the right-hand side).

Nat.div_le_iff_le_mul_add_pred theorem

(hb : 0 < b) : a / b ≤ c ↔ a ≤ b * c + (b - 1)

Full source

lemma div_le_iff_le_mul_add_pred (hb : 0 < b) : a / b ≤ c ↔ a ≤ b * c + (b - 1) := by
  rw [← Nat.lt_succ_iff, div_lt_iff_lt_mul hb, succ_mul, Nat.mul_comm]
  cases hb <;> exact Nat.lt_succ_iff

Natural Number Division Bound: $a/b \leq c \leftrightarrow a \leq bc + (b-1)$

Informal description

For any natural numbers $a$, $b$, and $c$, with $b > 0$, the inequality $a / b \leq c$ holds if and only if $a \leq b \times c + (b - 1)$.

Nat.div_lt_self' theorem

(a b : ℕ) : (a + 1) / (b + 2) < a + 1

Full source

/-- A version of `Nat.div_lt_self` using successors, rather than additional hypotheses. -/
lemma div_lt_self' (a b : ℕ) : (a + 1) / (b + 2) < a + 1 :=
  Nat.div_lt_self (Nat.succ_pos _) (Nat.succ_lt_succ (Nat.succ_pos _))

Successor-based division inequality: $(a + 1) / (b + 2) < a + 1$

Informal description

For any natural numbers $a$ and $b$, the division $(a + 1) / (b + 2)$ is strictly less than $a + 1$.

Nat.le_div_iff_mul_le' theorem

(hb : 0 < b) : a ≤ c / b ↔ a * b ≤ c

Full source

@[deprecated le_div_iff_mul_le (since := "2024-11-06")]
lemma le_div_iff_mul_le' (hb : 0 < b) : a ≤ c / b ↔ a * b ≤ c := le_div_iff_mul_le hb

Division-Multiplication Inequality for Natural Numbers

Informal description

For natural numbers $a$, $b$, and $c$ with $b > 0$, the inequality $a \leq c / b$ holds if and only if $a \times b \leq c$.

Nat.div_lt_iff_lt_mul' theorem

(hb : 0 < b) : a / b < c ↔ a < c * b

Full source

@[deprecated div_lt_iff_lt_mul (since := "2024-11-06")]
lemma div_lt_iff_lt_mul' (hb : 0 < b) : a / b < c ↔ a < c * b := div_lt_iff_lt_mul hb

Division-Multiplication Inequality for Natural Numbers

Informal description

For natural numbers $a$, $b$, and $c$ with $b > 0$, the inequality $a / b < c$ holds if and only if $a < c \cdot b$.

Nat.one_le_div_iff theorem

(hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a

Full source

lemma one_le_div_iff (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a := by rw [le_div_iff_mul_le hb, Nat.one_mul]

One is Less Than or Equal to Quotient if and Only if Divisor is Less Than or Equal to Dividend

Informal description

For any natural numbers $a$ and $b$ with $b > 0$, we have $1 \leq a / b$ if and only if $b \leq a$.

Nat.div_lt_one_iff theorem

(hb : 0 < b) : a / b < 1 ↔ a < b

Full source

lemma div_lt_one_iff (hb : 0 < b) : a / b < 1 ↔ a < b := by
  simp only [← Nat.not_le, one_le_div_iff hb]

Quotient Less Than One iff Dividend Less Than Divisor in Natural Numbers

Informal description

For any natural numbers $a$ and $b$ with $b > 0$, the inequality $a / b < 1$ holds if and only if $a < b$.

Nat.div_le_div_right theorem

(h : a ≤ b) : a / c ≤ b / c

Full source

protected lemma div_le_div_right (h : a ≤ b) : a / c ≤ b / c :=
  (c.eq_zero_or_pos.elim fun hc ↦ by simp [hc]) fun hc ↦
    (le_div_iff_mul_le hc).2 <| Nat.le_trans (Nat.div_mul_le_self _ _) h

Monotonicity of Natural Number Division with Respect to the Dividend

Informal description

For any natural numbers $a$, $b$, and $c$, if $a \leq b$, then the integer division of $a$ by $c$ is less than or equal to the integer division of $b$ by $c$, i.e., $a / c \leq b / c$.

Nat.lt_of_div_lt_div theorem

(h : a / c < b / c) : a < b

Full source

lemma lt_of_div_lt_div (h : a / c < b / c) : a < b :=
  Nat.lt_of_not_le fun hab ↦ Nat.not_le_of_lt h <| Nat.div_le_div_right hab

Strict Inequality Preservation Under Natural Number Division

Informal description

For any natural numbers $a$, $b$, and $c$, if the integer division of $a$ by $c$ is strictly less than the integer division of $b$ by $c$, then $a$ is strictly less than $b$, i.e., $a / c < b / c$ implies $a < b$.

Nat.div_eq_zero_iff theorem

: a / b = 0 ↔ b = 0 ∨ a < b

Full source

@[simp] protected lemma div_eq_zero_iff : a / b = 0 ↔ b = 0 ∨ a < b where
  mp h := by
    rw [← mod_add_div a b, h, Nat.mul_zero, Nat.add_zero, Decidable.or_iff_not_imp_left]
    exact mod_ltmod_lt _ ∘ Nat.pos_iff_ne_zero.2
  mpr := by
    obtain rfl | hb := Decidable.em (b = 0)
    · simp
    simp only [hb, false_or]
    rw [← Nat.mul_right_inj hb, ← Nat.add_left_cancel_iff, mod_add_div]
    simp +contextual [mod_eq_of_lt]

Zero Division Condition for Natural Numbers: $a/b = 0 \leftrightarrow b = 0 \lor a < b$

Informal description

For natural numbers $a$ and $b$, the division $a / b$ equals zero if and only if either $b$ is zero or $a$ is strictly less than $b$, i.e., $a / b = 0 \leftrightarrow (b = 0 \lor a < b)$.

Nat.div_ne_zero_iff theorem

: a / b ≠ 0 ↔ b ≠ 0 ∧ b ≤ a

Full source

protected lemma div_ne_zero_iff : a / b ≠ 0a / b ≠ 0 ↔ b ≠ 0 ∧ b ≤ a := by simp

Nonzero Division Condition for Natural Numbers: $a/b \neq 0 \leftrightarrow b \neq 0 \land b \leq a$

Informal description

For natural numbers $a$ and $b$, the division $a / b$ is nonzero if and only if $b$ is nonzero and $b$ is less than or equal to $a$.

Nat.div_pos_iff theorem

: 0 < a / b ↔ 0 < b ∧ b ≤ a

Full source

@[simp] protected lemma div_pos_iff : 0 < a / b ↔ 0 < b ∧ b ≤ a := by
  simp [Nat.pos_iff_ne_zero]

Positivity of Natural Number Division

Informal description

For natural numbers $a$ and $b$, the division $a / b$ is positive if and only if $b$ is positive and $b$ is less than or equal to $a$, i.e., $0 < a / b \leftrightarrow (0 < b \land b \leq a)$.

Nat.lt_mul_of_div_lt theorem

(h : a / c < b) (hc : 0 < c) : a < b * c

Full source

lemma lt_mul_of_div_lt (h : a / c < b) (hc : 0 < c) : a < b * c :=
  Nat.lt_of_not_ge <| Nat.not_le_of_gtNat.not_le_of_gt h ∘ (Nat.le_div_iff_mul_le hc).2

Division Bounds Multiplication in Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$ such that $a/c < b$ and $0 < c$, it holds that $a < b \cdot c$.

Nat.mul_div_le_mul_div_assoc theorem

(a b c : ℕ) : a * (b / c) ≤ a * b / c

Full source

lemma mul_div_le_mul_div_assoc (a b c : ℕ) : a * (b / c) ≤ a * b / c :=
  if hc0 : c = 0 then by simp [hc0] else
    (Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero hc0)).2
      (by rw [Nat.mul_assoc]; exact Nat.mul_le_mul_left _ (Nat.div_mul_le_self _ _))

Inequality for Multiplication and Division of Natural Numbers: $a \cdot (b / c) \leq (a \cdot b) / c$

Informal description

For any natural numbers $a$, $b$, and $c$, the inequality $a \cdot \left\lfloor \frac{b}{c} \right\rfloor \leq \left\lfloor \frac{a \cdot b}{c} \right\rfloor$ holds.

Nat.mul_div_cancel_left' theorem

(Hd : a ∣ b) : a * (b / a) = b

Full source

protected lemma mul_div_cancel_left' (Hd : a ∣ b) : a * (b / a) = b := by
  rw [Nat.mul_comm, Nat.div_mul_cancel Hd]

Division-Multiplication Cancellation for Natural Numbers

Informal description

For any natural numbers $a$ and $b$ such that $a$ divides $b$, it holds that $a \cdot (b / a) = b$.

Nat.lt_div_mul_add theorem

(hb : 0 < b) : a < a / b * b + b

Full source

lemma lt_div_mul_add (hb : 0 < b) : a < a / b * b + b := by
  rw [← Nat.succ_mul, ← Nat.div_lt_iff_lt_mul hb]; exact Nat.lt_succ_self _

Upper bound on natural division remainder: $a < b(\lfloor a/b \rfloor + 1)$

Informal description

For any natural numbers $a$ and $b$ with $b > 0$, we have $a < \left(\left\lfloor \frac{a}{b} \right\rfloor \times b\right) + b$.

Nat.div_left_inj theorem

(hda : d ∣ a) (hdb : d ∣ b) : a / d = b / d ↔ a = b

Full source

@[simp]
protected lemma div_left_inj (hda : d ∣ a) (hdb : d ∣ b) : a / d = b / d ↔ a = b := by
  refine ⟨fun h ↦ ?_, congrArg fun b ↦ b / d⟩
  rw [← Nat.mul_div_cancel' hda, ← Nat.mul_div_cancel' hdb, h]

Quotient Equality under Common Divisor in Natural Numbers

Informal description

For natural numbers $a$, $b$, and $d$, if $d$ divides both $a$ and $b$, then the equality of their quotients $a/d = b/d$ holds if and only if $a = b$.

Nat.sub_mul_div' theorem

(a b c : ℕ) : (a - b * c) / b = a / b - c

Full source

/-- TODO: Replace `Nat.sub_mul_div` in core. -/
lemma sub_mul_div' (a b c : ℕ) : (a - b * c) / b = a / b - c := by
  obtain h | h := Nat.le_total (b * c) a
  · rw [Nat.sub_mul_div _ _ _ h]
  · rw [Nat.sub_eq_zero_of_le h, Nat.zero_div]
    by_cases hn : b = 0
    · simp only [hn, Nat.div_zero, zero_le, Nat.sub_eq_zero_of_le]
    · have h2 : a / b ≤ (b * c) / b := Nat.div_le_div_right h
      rw [Nat.mul_div_cancel_left _ (zero_lt_of_ne_zero hn)] at h2
      rw [Nat.sub_eq_zero_of_le h2]

Division of Difference by Divisor: $\frac{a - b c}{b} = \frac{a}{b} - c$

Informal description

For any natural numbers $a$, $b$, and $c$, the following equality holds: \[ \frac{a - b \cdot c}{b} = \frac{a}{b} - c. \]

Nat.mul_sub_div_of_dvd theorem

(hc : c ≠ 0) (hcb : c ∣ b) (a : ℕ) : (c * a - b) / c = a - b / c

Full source

lemma mul_sub_div_of_dvd (hc : c ≠ 0) (hcb : c ∣ b) (a : ℕ) : (c * a - b) / c = a - b / c := by
  obtain ⟨_, hx⟩ := hcb
  simp only [hx, ← Nat.mul_sub_left_distrib, Nat.mul_div_right, zero_lt_of_ne_zero hc]

Division of a Scaled Difference by a Divisor

Informal description

For any natural numbers $a$, $b$, and $c$ with $c \neq 0$ and $c$ dividing $b$, we have \[ \frac{c \cdot a - b}{c} = a - \frac{b}{c}. \]

Nat.mul_add_mul_div_of_dvd theorem

(hb : b ≠ 0) (hd : d ≠ 0) (hba : b ∣ a) (hdc : d ∣ c) : (a * d + b * c) / (b * d) = a / b + c / d

Full source

lemma mul_add_mul_div_of_dvd (hb : b ≠ 0) (hd : d ≠ 0) (hba : b ∣ a) (hdc : d ∣ c) :
    (a * d + b * c) / (b * d) = a / b + c / d := by
  obtain ⟨n, hn⟩ := hba
  obtain ⟨_, hm⟩ := hdc
  rw [hn, hm, Nat.mul_assoc b n d, Nat.mul_comm n d, ← Nat.mul_assoc, ← Nat.mul_assoc,
    ← Nat.mul_add,
    Nat.mul_div_right _ (zero_lt_of_ne_zero hb),
    Nat.mul_div_right _ (zero_lt_of_ne_zero hd),
    Nat.mul_div_right _ (zero_lt_of_ne_zero <| Nat.mul_ne_zero hb hd)]

Division of Sum of Products by Product of Divisors Equals Sum of Quotients

Informal description

For any natural numbers $a, b, c, d$ with $b \neq 0$, $d \neq 0$, and such that $b$ divides $a$ and $d$ divides $c$, the following equality holds: \[ \frac{a \cdot d + b \cdot c}{b \cdot d} = \frac{a}{b} + \frac{c}{d}. \]

Nat.mul_sub_mul_div_of_dvd theorem

(hb : b ≠ 0) (hd : d ≠ 0) (hba : b ∣ a) (hdc : d ∣ c) : (a * d - b * c) / (b * d) = a / b - c / d

Full source

lemma mul_sub_mul_div_of_dvd (hb : b ≠ 0) (hd : d ≠ 0) (hba : b ∣ a) (hdc : d ∣ c) :
    (a * d - b * c) / (b * d)  = a / b - c / d := by
  obtain ⟨n, hn⟩ := hba
  obtain ⟨m, hm⟩ := hdc
  rw [hn, hm]
  rw [Nat.mul_assoc,Nat.mul_comm n d, ← Nat.mul_assoc,← Nat.mul_assoc, ← Nat.mul_sub_left_distrib,
    Nat.mul_div_right _ (zero_lt_of_ne_zero hb), Nat.mul_div_right _ (zero_lt_of_ne_zero hd),
    Nat.mul_div_right _ (zero_lt_of_ne_zero <| Nat.mul_ne_zero hb hd)]

Difference of Products Divided by Product Equals Difference of Quotients

Informal description

For any natural numbers $a, b, c, d$ with $b \neq 0$ and $d \neq 0$, if $b$ divides $a$ and $d$ divides $c$, then the following equality holds: \[ \frac{a \cdot d - b \cdot c}{b \cdot d} = \frac{a}{b} - \frac{c}{d}. \]

Nat.div_mul_right_comm theorem

(hba : b ∣ a) (c : ℕ) : a / b * c = a * c / b

Full source

protected lemma div_mul_right_comm (hba : b ∣ a) (c : ℕ) : a / b * c = a * c / b := by
  rw [Nat.mul_comm, ← Nat.mul_div_assoc _ hba, Nat.mul_comm]

Commutativity of Division and Multiplication under Divisibility: $(a / b) \cdot c = (a \cdot c) / b$ when $b \mid a$

Informal description

For any natural numbers $a$, $b$, and $c$, if $b$ divides $a$ (i.e., $b \mid a$), then $(a / b) \cdot c = (a \cdot c) / b$.

Nat.mul_div_right_comm theorem

(hba : b ∣ a) (c : ℕ) : a * c / b = a / b * c

Full source

protected lemma mul_div_right_comm (hba : b ∣ a) (c : ℕ) : a * c / b = a / b * c :=
  (Nat.div_mul_right_comm hba _).symm

Commutativity of Multiplication and Division under Divisibility: $(a \cdot c)/b = (a/b) \cdot c$ when $b \mid a$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $b$ divides $a$ (i.e., $b \mid a$), the following equality holds: \[ \frac{a \cdot c}{b} = \frac{a}{b} \cdot c. \]

Nat.div_mul_div_comm theorem

: b ∣ a → d ∣ c → (a / b) * (c / d) = (a * c) / (b * d)

Full source

lemma div_mul_div_comm : b ∣ a → d ∣ c → (a / b) * (c / d) = (a * c) / (b * d) := by
  rintro ⟨x, rfl⟩ ⟨y, rfl⟩
  obtain rfl | hb := b.eq_zero_or_pos
  · simp
  obtain rfl | hd := d.eq_zero_or_pos
  · simp
  rw [Nat.mul_div_cancel_left _ hb, Nat.mul_div_cancel_left _ hd, Nat.mul_assoc b,
    Nat.mul_left_comm x, ← Nat.mul_assoc b, Nat.mul_div_cancel_left _ (Nat.mul_pos hb hd)]

Quotient Multiplication Commutes with Division: $(a/b) \cdot (c/d) = (a \cdot c)/(b \cdot d)$

Informal description

For any natural numbers $a, b, c, d$ such that $b$ divides $a$ and $d$ divides $c$, the product of the quotients $(a / b) \cdot (c / d)$ is equal to the quotient of the products $(a \cdot c) / (b \cdot d)$.

Nat.mul_div_mul_comm theorem

(hba : b ∣ a) (hdc : d ∣ c) : a * c / (b * d) = a / b * (c / d)

Full source

protected lemma mul_div_mul_comm (hba : b ∣ a) (hdc : d ∣ c) : a * c / (b * d) = a / b * (c / d) :=
  (div_mul_div_comm hba hdc).symm

Commutativity of Multiplication and Division: $(a \cdot c)/(b \cdot d) = (a/b) \cdot (c/d)$

Informal description

For any natural numbers $a, b, c, d$ such that $b$ divides $a$ and $d$ divides $c$, the quotient $(a \cdot c) / (b \cdot d)$ is equal to the product $(a / b) \cdot (c / d)$.

Nat.div_mul_div_le_div theorem

(a b c : ℕ) : a / c * b / a ≤ b / c

Full source

lemma div_mul_div_le_div (a b c : ℕ) : a / c * b / a ≤ b / c := by
  obtain rfl | ha := Nat.eq_zero_or_pos a
  · simp
  · calc
      a / c * b / a ≤ b * a / c / a :=
        Nat.div_le_div_right (by rw [Nat.mul_comm]; exact mul_div_le_mul_div_assoc _ _ _)
      _ = b / c := by rw [Nat.div_div_eq_div_mul, Nat.mul_comm b, Nat.mul_comm c,
          Nat.mul_div_mul_left _ _ ha]

Inequality for Nested Division and Multiplication of Natural Numbers: $\frac{(a/c) \cdot b}{a} \leq b/c$

Informal description

For any natural numbers $a$, $b$, and $c$, the inequality $\frac{\lfloor a/c \rfloor \cdot b}{a} \leq \frac{b}{c}$ holds.

Nat.le_half_of_half_lt_sub theorem

(h : a / 2 < a - b) : b ≤ a / 2

Full source

lemma le_half_of_half_lt_sub (h : a / 2 < a - b) : b ≤ a / 2 := by
  omega

Upper Bound on Natural Number from Half Difference Inequality

Informal description

For any natural numbers $a$ and $b$, if the half of $a$ is less than $a - b$, then $b$ is less than or equal to half of $a$, i.e., if $\frac{a}{2} < a - b$, then $b \leq \frac{a}{2}$.

Nat.half_le_of_sub_le_half theorem

(h : a - b ≤ a / 2) : a / 2 ≤ b

Full source

lemma half_le_of_sub_le_half (h : a - b ≤ a / 2) : a / 2 ≤ b := by
  omega

Lower Bound on Natural Number from Half Difference Inequality

Informal description

For any natural numbers $a$ and $b$, if the difference $a - b$ is less than or equal to half of $a$, then half of $a$ is less than or equal to $b$, i.e., if $a - b \leq \frac{a}{2}$, then $\frac{a}{2} \leq b$.

Nat.div_le_of_le_mul' theorem

(h : m ≤ k * n) : m / k ≤ n

Full source

protected lemma div_le_of_le_mul' (h : m ≤ k * n) : m / k ≤ n := by
  obtain rfl | hk := k.eq_zero_or_pos
  · simp
  · refine Nat.le_of_mul_le_mul_left ?_ hk
    calc
      k * (m / k) ≤ m % k + k * (m / k) := Nat.le_add_left _ _
      _ = m := mod_add_div _ _
      _ ≤ k * n := h

Upper Bound on Integer Division of Natural Numbers

Informal description

For any natural numbers $m$, $k$, and $n$, if $m \leq k \cdot n$, then the integer division of $m$ by $k$ is less than or equal to $n$, i.e., $m / k \leq n$.

Nat.div_le_div_of_mul_le_mul theorem

(hd : d ≠ 0) (hdc : d ∣ c) (h : a * d ≤ c * b) : a / b ≤ c / d

Full source

protected lemma div_le_div_of_mul_le_mul (hd : d ≠ 0) (hdc : d ∣ c) (h : a * d ≤ c * b) :
    a / b ≤ c / d :=
  Nat.div_le_of_le_mul' <| by
    rwa [← Nat.mul_div_assoc _ hdc, Nat.le_div_iff_mul_le (Nat.pos_iff_ne_zero.2 hd), b.mul_comm]

Monotonicity of Natural Number Division under Multiplicative Inequality

Informal description

For any natural numbers $a, b, c, d$ with $d \neq 0$ and $d$ dividing $c$, if $a \cdot d \leq c \cdot b$, then the integer division of $a$ by $b$ is less than or equal to the integer division of $c$ by $d$, i.e., $a / b \leq c / d$.

Nat.div_le_self' theorem

(m n : ℕ) : m / n ≤ m

Full source

protected lemma div_le_self' (m n : ℕ) : m / n ≤ m := by
  obtain rfl | hn := n.eq_zero_or_pos
  · simp
  · refine Nat.div_le_of_le_mul' ?_
    calc
      m = 1 * m := by rw [Nat.one_mul]
      _ ≤ n * m := Nat.mul_le_mul_right _ hn

Division of Natural Numbers is Bounded by Dividend

Informal description

For any natural numbers $m$ and $n$, the integer division of $m$ by $n$ is less than or equal to $m$, i.e., $m / n \leq m$.

Nat.two_mul_odd_div_two theorem

(hn : n % 2 = 1) : 2 * (n / 2) = n - 1

Full source

lemma two_mul_odd_div_two (hn : n % 2 = 1) : 2 * (n / 2) = n - 1 := by
  conv => rhs; rw [← Nat.mod_add_div n 2, hn, Nat.add_sub_cancel_left]

Double of Half of Odd Natural Number Equals Number Minus One

Informal description

For any natural number $n$ such that $n$ is odd (i.e., $n \mod 2 = 1$), we have $2 \cdot \left\lfloor \frac{n}{2} \right\rfloor = n - 1$.

Nat.div_eq_self theorem

: m / n = m ↔ m = 0 ∨ n = 1

Full source

lemma div_eq_self : m / n = m ↔ m = 0 ∨ n = 1 := by
  constructor
  · intro
    match n with
    | 0 => simp_all
    | 1 => right; rfl
    | n+2 =>
      left
      have : m / (n + 2) ≤ m / 2 := div_le_div_left (by simp) (by decide)
      refine eq_zero_of_le_half ?_
      simp_all
  · rintro (rfl | rfl) <;> simp

Division Equals Dividend Condition for Natural Numbers

Informal description

For natural numbers $m$ and $n$, the division $m / n$ equals $m$ if and only if either $m = 0$ or $n = 1$.

Nat.div_eq_sub_mod_div theorem

: m / n = (m - m % n) / n

Full source

lemma div_eq_sub_mod_div : m / n = (m - m % n) / n := by
  obtain rfl | hn := n.eq_zero_or_pos
  · rw [Nat.div_zero, Nat.div_zero]
  · have : m - m % n = n * (m / n) := by
      rw [Nat.sub_eq_iff_eq_add (Nat.mod_le _ _), Nat.add_comm, mod_add_div]
    rw [this, mul_div_right _ hn]

Division as Subtraction of Remainder Divided by Divisor

Informal description

For any natural numbers $m$ and $n$, the division $m / n$ equals the division of $(m - m \% n)$ by $n$, where $m \% n$ denotes the remainder of $m$ divided by $n$. In other words: \[ m / n = (m - (m \% n)) / n \]

Nat.mul_le_of_le_div theorem

(k x y : ℕ) (h : x ≤ y / k) : x * k ≤ y

Full source

protected lemma mul_le_of_le_div (k x y : ℕ) (h : x ≤ y / k) : x * k ≤ y := by
  if hk : k = 0 then
    rw [hk, Nat.mul_zero]; exact zero_le _
  else
    rwa [← le_div_iff_mul_le (Nat.pos_iff_ne_zero.2 hk)]

Multiplication Bound from Division Inequality in Natural Numbers

Informal description

For any natural numbers $k$, $x$, and $y$, if $x \leq y / k$, then $x \cdot k \leq y$.

Nat.div_le_iff_le_mul_of_dvd theorem

(hb : b ≠ 0) (hba : b ∣ a) : a / b ≤ c ↔ a ≤ c * b

Full source

theorem div_le_iff_le_mul_of_dvd (hb : b ≠ 0) (hba : b ∣ a) : a / b ≤ c ↔ a ≤ c * b := by
  obtain ⟨_, hx⟩ := hba
  simp only [hx]
  rw [Nat.mul_div_right _ (zero_lt_of_ne_zero hb), Nat.mul_comm]
  exact ⟨mul_le_mul_right b, fun h ↦ Nat.le_of_mul_le_mul_right h (zero_lt_of_ne_zero hb)⟩

Division Inequality under Divisibility Condition: $a / b \leq c \leftrightarrow a \leq c \cdot b$ when $b \mid a$ and $b \neq 0$

Informal description

For natural numbers $a$, $b$, and $c$, if $b \neq 0$ and $b$ divides $a$, then the inequality $a / b \leq c$ holds if and only if $a \leq c \cdot b$.

Nat.div_lt_div_right theorem

(ha : a ≠ 0) : a ∣ b → a ∣ c → (b / a < c / a ↔ b < c)

Full source

protected lemma div_lt_div_right (ha : a ≠ 0) : a ∣ b → a ∣ c → (b / a < c / a ↔ b < c) := by
  rintro ⟨d, rfl⟩ ⟨e, rfl⟩; simp [Nat.mul_div_cancel, Nat.pos_iff_ne_zero.2 ha]

Division Preserves Order for Common Divisors in Natural Numbers

Informal description

For any nonzero natural number $a$, if $a$ divides both $b$ and $c$, then the inequality $b/a < c/a$ holds if and only if $b < c$.

Nat.div_lt_div_left theorem

(ha : a ≠ 0) (hba : b ∣ a) (hca : c ∣ a) : a / b < a / c ↔ c < b

Full source

protected lemma div_lt_div_left (ha : a ≠ 0) (hba : b ∣ a) (hca : c ∣ a) :
    a / b < a / c ↔ c < b := by
  obtain ⟨d, hd⟩ := hba
  obtain ⟨e, he⟩ := hca
  rw [Nat.div_eq_of_eq_mul_right _ hd, Nat.div_eq_of_eq_mul_right _ he,
    Nat.lt_iff_lt_of_mul_eq_mul ha hd he] <;>
    rw [Nat.pos_iff_ne_zero] <;> rintro rfl <;> simp_all

Order Reversal in Division of Common Divisors: $a/b < a/c \leftrightarrow c < b$ when $b,c \mid a$ and $a \neq 0$

Informal description

For any nonzero natural number $a$, if $b$ and $c$ both divide $a$, then the inequality $a/b < a/c$ holds if and only if $c < b$.

Nat.lt_div_iff_mul_lt_of_dvd theorem

(hc : c ≠ 0) (hcb : c ∣ b) : a < b / c ↔ a * c < b

Full source

theorem lt_div_iff_mul_lt_of_dvd (hc : c ≠ 0) (hcb : c ∣ b) : a < b / c ↔ a * c < b := by
  simp [← Nat.div_lt_div_right _ _ hcb, hc, Nat.pos_iff_ne_zero, Nat.dvd_mul_left]

Division Inequality under Divisibility: $a < b/c \leftrightarrow a \times c < b$ when $c \mid b$ and $c \neq 0$

Informal description

For any nonzero natural number $c$ that divides $b$, the inequality $a < b / c$ holds if and only if $a \times c < b$.

Nat.pow_lt_pow_right theorem

(ha : 1 < a) (h : m < n) : a ^ m < a ^ n

Full source

protected lemma pow_lt_pow_right (ha : 1 < a) (h : m < n) : a ^ m < a ^ n :=
  (Nat.pow_lt_pow_iff_right ha).2 h

Exponentiation is Strictly Increasing for Base Greater Than One

Informal description

For natural numbers $a$, $m$, and $n$, if $1 < a$ and $m < n$, then $a^m < a^n$.

Nat.pow_le_pow_iff_left theorem

{n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b

Full source

protected lemma pow_le_pow_iff_left {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b where
  mp := by simpa only [← Nat.not_le, Decidable.not_imp_not] using (Nat.pow_lt_pow_left · hn)
  mpr h := Nat.pow_le_pow_left h _

Natural Number Power Inequality: $a^n \leq b^n \leftrightarrow a \leq b$ for $n \neq 0$

Informal description

For natural numbers $a$, $b$, and a nonzero natural number $n$, the inequality $a^n \leq b^n$ holds if and only if $a \leq b$.

Nat.pow_lt_pow_iff_left theorem

(hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b

Full source

protected lemma pow_lt_pow_iff_left (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b := by
  simp only [← Nat.not_le, Nat.pow_le_pow_iff_left hn]

Strict Power Inequality for Natural Numbers: $a^n < b^n \leftrightarrow a < b$ when $n \neq 0$

Informal description

For natural numbers $a$, $b$, and a nonzero natural number $n$, the inequality $a^n < b^n$ holds if and only if $a < b$.

Nat.pow_eq_zero theorem

{a : ℕ} : ∀ {n : ℕ}, a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

Full source

@[simp high] protected lemma pow_eq_zero {a : ℕ} : ∀ {n : ℕ}, a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
  | 0 => by simp
  | n + 1 => by rw [Nat.pow_succ, mul_eq_zero, Nat.pow_eq_zero]; omega

Zero Power Condition for Natural Numbers: $a^n = 0 \leftrightarrow (a = 0 \land n \neq 0)$

Informal description

For any natural numbers $a$ and $n$, the power $a^n$ equals zero if and only if $a = 0$ and $n \neq 0$.

Nat.le_self_pow theorem

(hn : n ≠ 0) : ∀ a : ℕ, a ≤ a ^ n

Full source

lemma le_self_pow (hn : n ≠ 0) : ∀ a : ℕ, a ≤ a ^ n
  | 0 => zero_le _
  | a + 1 => by simpa using Nat.pow_le_pow_right a.succ_pos (Nat.one_le_iff_ne_zero.2 hn)

Natural number is less than or equal to its own power ($a \leq a^n$ for $n \neq 0$)

Informal description

For any natural number $a$ and any nonzero natural number $n$, we have $a \leq a^n$.

Nat.one_le_pow theorem

(n m : ℕ) (h : 0 < m) : 1 ≤ m ^ n

Full source

lemma one_le_pow (n m : ℕ) (h : 0 < m) : 1 ≤ m ^ n := by simpa using Nat.pow_le_pow_left h n

Lower bound on positive natural number powers: $1 \leq m^n$

Informal description

For any natural numbers $n$ and $m$ with $m > 0$, we have $1 \leq m^n$.

Nat.one_le_pow' theorem

(n m : ℕ) : 1 ≤ (m + 1) ^ n

Full source

lemma one_le_pow' (n m : ℕ) : 1 ≤ (m + 1) ^ n := one_le_pow n (m + 1) (succ_pos m)

Lower bound on successor powers: $1 \leq (m+1)^n$

Informal description

For any natural numbers $n$ and $m$, we have $1 \leq (m + 1)^n$.

Nat.one_lt_pow theorem

(hn : n ≠ 0) (ha : 1 < a) : 1 < a ^ n

Full source

lemma one_lt_pow (hn : n ≠ 0) (ha : 1 < a) : 1 < a ^ n := by simpa using Nat.pow_lt_pow_left ha hn

Exponentiation of Numbers Greater Than One Yields Results Greater Than One

Informal description

For any natural numbers $a$ and $n$, if $n \neq 0$ and $1 < a$, then $1 < a^n$.

Nat.two_pow_succ theorem

(n : ℕ) : 2 ^ (n + 1) = 2 ^ n + 2 ^ n

Full source

lemma two_pow_succ (n : ℕ) : 2 ^ (n + 1) = 2 ^ n + 2 ^ n := by simp [Nat.pow_succ, Nat.mul_two]

Exponential Doubling Identity: $2^{n+1} = 2^n + 2^n$

Informal description

For any natural number $n$, the power $2^{n+1}$ is equal to the sum of $2^n$ and $2^n$, i.e., $2^{n+1} = 2^n + 2^n$.

Nat.one_lt_pow' theorem

(n m : ℕ) : 1 < (m + 2) ^ (n + 1)

Full source

lemma one_lt_pow' (n m : ℕ) : 1 < (m + 2) ^ (n + 1) :=
  one_lt_pow n.succ_ne_zero (Nat.lt_of_sub_eq_succ rfl)

Exponentiation of Numbers Greater Than or Equal to Two Yields Results Greater Than One

Informal description

For any natural numbers $n$ and $m$, the expression $(m + 2)^{n + 1}$ is strictly greater than 1.

Nat.one_lt_pow_iff theorem

{n : ℕ} (hn : n ≠ 0) : ∀ {a}, 1 < a ^ n ↔ 1 < a

Full source

@[simp] lemma one_lt_pow_iff {n : ℕ} (hn : n ≠ 0) : ∀ {a}, 1 < a ^ n ↔ 1 < a
 | 0 => by simp [Nat.zero_pow (Nat.pos_of_ne_zero hn)]
 | 1 => by simp
 | a + 2 => by simp [one_lt_pow hn]

Characterization of when $1 < a^n$: $1 < a^n \leftrightarrow 1 < a$ for $n \neq 0$

Informal description

For any natural number $n \neq 0$ and any natural number $a$, we have $1 < a^n$ if and only if $1 < a$.

Nat.one_lt_two_pow' theorem

(n : ℕ) : 1 < 2 ^ (n + 1)

Full source

lemma one_lt_two_pow' (n : ℕ) : 1 < 2 ^ (n + 1) := one_lt_pow n.succ_ne_zero (by decide)

Exponential Growth of Powers of Two: $1 < 2^{n+1}$

Informal description

For any natural number $n$, the inequality $1 < 2^{n+1}$ holds.

Nat.mul_lt_mul_pow_succ theorem

(ha : 0 < a) (hb : 1 < b) : n * b < a * b ^ (n + 1)

Full source

lemma mul_lt_mul_pow_succ (ha : 0 < a) (hb : 1 < b) : n * b < a * b ^ (n + 1) := by
  rw [Nat.pow_succ, ← Nat.mul_assoc, Nat.mul_lt_mul_right (Nat.lt_trans Nat.zero_lt_one hb)]
  exact Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_left _ ha)
    ((Nat.mul_lt_mul_left ha).2 <| Nat.lt_pow_self hb)

Inequality for Multiplication and Power Successor: $n \cdot b < a \cdot b^{n+1}$

Informal description

For any natural numbers $a$, $b$, and $n$, if $0 < a$ and $1 < b$, then $n \cdot b < a \cdot b^{n+1}$.

Nat.sq_sub_sq theorem

(a b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

Full source

lemma sq_sub_sq (a b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
  simpa [Nat.pow_succ] using Nat.mul_self_sub_mul_self_eq a b

Difference of Squares Identity for Natural Numbers: $a^2 - b^2 = (a+b)(a-b)$

Informal description

For any natural numbers $a$ and $b$, the difference of squares $a^2 - b^2$ equals $(a + b)(a - b)$.

Nat.div_pow theorem

(h : a ∣ b) : (b / a) ^ c = b ^ c / a ^ c

Full source

protected lemma div_pow (h : a ∣ b) : (b / a) ^ c = b ^ c / a ^ c := by
  obtain rfl | hc := c.eq_zero_or_pos
  · simp
  obtain rfl | ha := a.eq_zero_or_pos
  · simp [Nat.zero_pow hc]
  refine (Nat.div_eq_of_eq_mul_right (Nat.pow_pos ha) ?_).symm
  rw [← Nat.mul_pow, Nat.mul_div_cancel_left' h]

Power of Quotient Equals Quotient of Powers for Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$ such that $a$ divides $b$, it holds that $(b / a)^c = b^c / a^c$.

Nat.pow_pos_iff theorem

: 0 < a ^ n ↔ 0 < a ∨ n = 0

Full source

protected lemma pow_pos_iff : 0 < a ^ n ↔ 0 < a ∨ n = 0 := by
  simp [Nat.pos_iff_ne_zero, Decidable.imp_iff_not_or]

Positivity of Natural Number Powers: $0 < a^n \leftrightarrow (0 < a \lor n = 0)$

Informal description

For any natural numbers $a$ and $n$, the power $a^n$ is positive if and only if either $a$ is positive or $n$ is zero.

Nat.pow_self_pos theorem

: 0 < n ^ n

Full source

lemma pow_self_pos : 0 < n ^ n := by simp [Nat.pow_pos_iff, n.eq_zero_or_pos.symm]

Positivity of Natural Number Powers: $0 < n^n$

Informal description

For any natural number $n$, the power $n^n$ is strictly positive, i.e., $0 < n^n$.

Nat.pow_self_mul_pow_self_le theorem

: m ^ m * n ^ n ≤ (m + n) ^ (m + n)

Full source

lemma pow_self_mul_pow_self_le : m ^ m * n ^ n ≤ (m + n) ^ (m + n) := by
  rw [Nat.pow_add]
  exact Nat.mul_le_mul (Nat.pow_le_pow_left (le_add_right ..) _)
    (Nat.pow_le_pow_left (le_add_left ..) _)

Inequality for Product of Powers: $m^m n^n \leq (m+n)^{m+n}$

Informal description

For any natural numbers $m$ and $n$, the product of $m^m$ and $n^n$ is less than or equal to $(m + n)^{m + n}$.

Nat.rec_zero theorem

{C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) : Nat.rec h0 h 0 = h0

Full source

@[simp]
lemma rec_zero {C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) : Nat.rec h0 h 0 = h0 := rfl

Base Case of Natural Number Recursion

Informal description

For any type family $C : \mathbb{N} \to \text{Sort}*$ and given $h_0 : C(0)$ and $h : \forall n, C(n) \to C(n+1)$, the recursion principle for natural numbers satisfies $\text{Nat.rec}\ h_0\ h\ 0 = h_0$.

Nat.rec_add_one theorem

{C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) (n : ℕ) : Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n)

Full source

lemma rec_add_one {C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) (n : ℕ) :
    Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n) := rfl

Recursion Step for Natural Numbers

Informal description

For any type family $C : \mathbb{N} \to \text{Sort}*$, given a base case $h_0 : C(0)$ and a step function $h : \forall n, C(n) \to C(n+1)$, the recursion principle satisfies $\text{Nat.rec}\ h_0\ h\ (n+1) = h\ n\ (\text{Nat.rec}\ h_0\ h\ n)$ for any natural number $n$.

Nat.rec_one theorem

{C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) : Nat.rec (motive := C) h0 h 1 = h 0 h0

Full source

@[simp] lemma rec_one {C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) :
    Nat.rec (motive := C) h0 h 1 = h 0 h0 := rfl

Recursion Principle for Natural Numbers at One

Informal description

For any type family $C : \mathbb{N} \to \text{Sort}^*$, given a base case $h_0 : C(0)$ and a recursive step $h : \forall n, C(n) \to C(n+1)$, the recursion principle applied to $1$ equals $h$ applied to $0$ and $h_0$, i.e., $\text{Nat.rec}\ h_0\ h\ 1 = h\ 0\ h_0$.

Nat.leRec definition

 {n} {motive : (m : ℕ) → n ≤ m → Sort*} (refl : motive n (Nat.le_refl _))
  (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h)) : ∀ {m} (h : n ≤ m), motive m h

Full source

/-- Recursion starting at a non-zero number: given a map `C k → C (k+1)` for each `k ≥ n`,
there is a map from `C n` to each `C m`, `n ≤ m`.

This is a version of `Nat.le.rec` that works for `Sort u`.
Similarly to `Nat.le.rec`, it can be used as
```
induction hle using Nat.leRec with
| refl => sorry
| le_succ_of_le hle ih => sorry
```
-/
@[elab_as_elim]
def leRec {n} {motive : (m : ℕ) → n ≤ m → Sort*}
    (refl : motive n (Nat.le_refl _))
    (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h)) :
    ∀ {m} (h : n ≤ m), motive m h
  | 0, H => Nat.eq_zero_of_le_zero H ▸ refl
  | m + 1, H =>
    (le_succ_iff.1 H).by_cases
      (fun h : n ≤ m ↦ le_succ_of_le h <| leRec refl le_succ_of_le h)
      (fun h : n = m + 1 ↦ h ▸ refl)

Recursion on natural numbers starting at a non-zero base case

Informal description

Given a natural number $n$ and a family of types $C(m)$ indexed by natural numbers $m \geq n$, along with: 1. A term `refl` of type $C(n)$ (the base case), 2. A function `le_succ_of_le` that for any $k \geq n$ and a proof $h$ that $n \leq k$, takes a term of $C(k)$ and produces a term of $C(k+1)$, the function `Nat.leRec` constructs, for any $m \geq n$ and proof $h$ that $n \leq m$, a term of $C(m)$. This is done by recursively applying `le_succ_of_le` starting from `refl`.

Nat.leRec_eq_leRec theorem

: @Nat.leRec.{0} = @Nat.le.rec

Full source

theorem leRec_eq_leRec : @Nat.leRec.{0} = @Nat.le.rec := rfl

Equality of Specialized Recursion Principles for Natural Numbers

Informal description

The recursion principle `Nat.leRec` for natural numbers starting at a non-zero base case is equal to the standard recursion principle `Nat.le.rec` when specialized to universe level 0.

Nat.leRec_self theorem

 {n} {motive : (m : ℕ) → n ≤ m → Sort*} (refl : motive n (Nat.le_refl _))
  (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h)) :
  (leRec (motive := motive) refl le_succ_of_le (Nat.le_refl _) : motive n (Nat.le_refl _)) = refl

Full source

@[simp]
lemma leRec_self {n} {motive : (m : ℕ) → n ≤ m → Sort*}
    (refl : motive n (Nat.le_refl _))
    (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h)) :
    (leRec (motive := motive) refl le_succ_of_le (Nat.le_refl _) :
    motive n (Nat.le_refl _)) = refl := by
  cases n <;> simp [leRec, Or.by_cases, dif_neg]

Base Case Preservation in Natural Number Recursion Starting at $n$

Informal description

For any natural number $n$ and a family of types $C(m)$ indexed by natural numbers $m \geq n$, given: 1. A term `refl` of type $C(n)$ (the base case), 2. A function `le_succ_of_le` that for any $k \geq n$ and a proof $h$ that $n \leq k$, takes a term of $C(k)$ and produces a term of $C(k+1)$, the recursion term `Nat.leRec refl le_succ_of_le` applied to the reflexive proof `Nat.le_refl n` yields the base case `refl`, i.e., $$\text{Nat.leRec refl le\_succ\_of\_le (Nat.le\_refl n)} = \text{refl}.$$

Nat.leRec_succ theorem

 {n} {motive : (m : ℕ) → n ≤ m → Sort*} (refl : motive n (Nat.le_refl _))
  (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h)) (h1 : n ≤ m) {h2 : n ≤ m + 1} :
  (leRec (motive := motive) refl le_succ_of_le h2) = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)

Full source

@[simp]
lemma leRec_succ {n} {motive : (m : ℕ) → n ≤ m → Sort*}
    (refl : motive n (Nat.le_refl _))
    (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h))
    (h1 : n ≤ m) {h2 : n ≤ m + 1} :
    (leRec (motive := motive) refl le_succ_of_le h2) =
      le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1) := by
  conv =>
    lhs
    rw [leRec, Or.by_cases, dif_pos h1]

Recursion Step for Natural Numbers Starting at Non-Zero Base

Informal description

Given a natural number $n$ and a family of types $C(m)$ indexed by natural numbers $m \geq n$, along with: 1. A term `refl` of type $C(n)$ (the base case), 2. A function `le_succ_of_le` that for any $k \geq n$ and a proof $h$ that $n \leq k$, takes a term of $C(k)$ and produces a term of $C(k+1)$, then for any $m \geq n$ with proof $h_1$ that $n \leq m$, and any proof $h_2$ that $n \leq m+1$, the recursive construction satisfies: \[ \text{leRec}(C, \text{refl}, \text{le\_succ\_of\_le}, h_2) = \text{le\_succ\_of\_le}(h_1, \text{leRec}(C, \text{refl}, \text{le\_succ\_of\_le}, h_1)) \]

Nat.leRec_succ' theorem

 {n} {motive : (m : ℕ) → n ≤ m → Sort*} (refl le_succ_of_le) :
  (leRec (motive := motive) refl le_succ_of_le (le_succ _)) = le_succ_of_le _ refl

Full source

lemma leRec_succ' {n} {motive : (m : ℕ) → n ≤ m → Sort*} (refl le_succ_of_le) :
    (leRec (motive := motive) refl le_succ_of_le (le_succ _)) = le_succ_of_le _ refl := by
  rw [leRec_succ, leRec_self]

Recursion Step for Successor Case Starting at Base Point $n$

Informal description

For any natural number $n$ and a family of types $C(m)$ indexed by natural numbers $m \geq n$, given: 1. A term `refl` of type $C(n)$ (the base case), 2. A function `le_succ_of_le` that for any $k \geq n$ and a proof $h$ that $n \leq k$, takes a term of $C(k)$ and produces a term of $C(k+1)$, the recursive construction satisfies: \[ \text{leRec}(C, \text{refl}, \text{le\_succ\_of\_le}, \text{le\_succ}(n)) = \text{le\_succ\_of\_le}(n, \text{refl}) \] where $\text{le\_succ}(n)$ is the proof that $n \leq n+1$.

Nat.leRec_trans theorem

 {n m k} {motive : (m : ℕ) → n ≤ m → Sort*} (refl le_succ_of_le) (hnm : n ≤ m) (hmk : m ≤ k) :
  leRec (motive := motive) refl le_succ_of_le (Nat.le_trans hnm hmk) =
    leRec (leRec refl (fun _ h => le_succ_of_le h) hnm) (fun _ h => le_succ_of_le <| Nat.le_trans hnm h) hmk

Full source

lemma leRec_trans {n m k} {motive : (m : ℕ) → n ≤ m → Sort*} (refl le_succ_of_le)
    (hnm : n ≤ m) (hmk : m ≤ k) :
    leRec (motive := motive) refl le_succ_of_le (Nat.le_trans hnm hmk) =
      leRec
        (leRec refl (fun _ h => le_succ_of_le h) hnm)
        (fun _ h => le_succ_of_le <| Nat.le_trans hnm h) hmk := by
  induction hmk with
  | refl => rw [leRec_self]
  | step hmk ih => rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]

Transitivity of Recursion on Natural Numbers Starting at Non-Zero Base

Informal description

Given natural numbers $n \leq m \leq k$ and a family of types $C(l)$ indexed by natural numbers $l \geq n$, along with: 1. A term `refl` of type $C(n)$ (the base case), 2. A function `le_succ_of_le` that for any $l \geq n$ and a proof $h$ that $n \leq l$, takes a term of $C(l)$ and produces a term of $C(l+1)$, the recursive construction satisfies: \[ \text{leRec}(C, \text{refl}, \text{le\_succ\_of\_le}, \text{trans}(h_{nm}, h_{mk})) = \text{leRec}(\text{leRec}(C, \text{refl}, \text{le\_succ\_of\_le}, h_{nm}), \text{le\_succ\_of\_le} \circ \text{trans}(h_{nm}), h_{mk}) \] where $\text{trans}(h_{nm}, h_{mk})$ is the proof that $n \leq k$ obtained by transitivity from $h_{nm}: n \leq m$ and $h_{mk}: m \leq k$.

Nat.leRec_succ_left theorem

 {motive : (m : ℕ) → n ≤ m → Sort*} (refl le_succ_of_le) {m} (h1 : n ≤ m) (h2 : n + 1 ≤ m) :
  -- the `@` is needed for this to elaborate, even though we only provide explicit arguments!@leRec _ _
      (le_succ_of_le (Nat.le_refl _) refl) (fun _ h ih => le_succ_of_le (le_of_succ_le h) ih) _ h2 =
    leRec (motive := motive) refl le_succ_of_le h1

Full source

lemma leRec_succ_left {motive : (m : ℕ) → n ≤ m → Sort*}
    (refl le_succ_of_le) {m} (h1 : n ≤ m) (h2 : n + 1 ≤ m) :
    -- the `@` is needed for this to elaborate, even though we only provide explicit arguments!
    @leRec _ _ (le_succ_of_le (Nat.le_refl _) refl)
        (fun _ h ih => le_succ_of_le (le_of_succ_le h) ih) _ h2 =
      leRec (motive := motive) refl le_succ_of_le h1 := by
  rw [leRec_trans _ _ (le_succ n) h2, leRec_succ']

Recursion Equality for Successor Base Case in Natural Numbers

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$ and $n+1 \leq m$, and for any family of types $C(k)$ indexed by natural numbers $k \geq n$, given: 1. A term `refl` of type $C(n)$ (the base case), 2. A function `le_succ_of_le` that for any $k \geq n$ and a proof $h$ that $n \leq k$, takes a term of $C(k)$ and produces a term of $C(k+1)$, the recursive construction satisfies: \[ \text{leRec}(C, \text{le\_succ\_of\_le}(n \leq n, \text{refl}), \lambda h \text{ ih}, \text{le\_succ\_of\_le}(\text{le\_of\_succ\_le}(h), \text{ih}), n+1 \leq m) = \text{leRec}(C, \text{refl}, \text{le\_succ\_of\_le}, n \leq m) \] where $\text{le\_of\_succ\_le}(h)$ is the proof that $n \leq k$ obtained from $h : n+1 \leq k$.

Nat.leRecOn definition

{C : ℕ → Sort*} {n : ℕ} : ∀ {m}, n ≤ m → (∀ {k}, C k → C (k + 1)) → C n → C m

Full source

/-- Recursion starting at a non-zero number: given a map `C k → C (k + 1)` for each `k`,
there is a map from `C n` to each `C m`, `n ≤ m`. For a version where the assumption is only made
when `k ≥ n`, see `Nat.leRec`. -/
@[elab_as_elim]
def leRecOn {C : ℕ → Sort*} {n : ℕ} : ∀ {m}, n ≤ m → (∀ {k}, C k → C (k + 1)) → C n → C m :=
  fun h of_succ self => Nat.leRec self (fun _ _ => @of_succ _) h

Recursion on natural numbers starting at a base case

Informal description

Given a family of types $C(k)$ indexed by natural numbers $k$, a natural number $n$, and a natural number $m$ with $n \leq m$, the function `Nat.leRecOn` constructs an element of $C(m)$ from: 1. A proof $h$ that $n \leq m$, 2. A function `of_succ` that for any $k$ takes an element of $C(k)$ and produces an element of $C(k+1)$, 3. An element `self` of $C(n)$ (the base case). This is done by recursively applying `of_succ` starting from `self` and using the proof $h$ to ensure termination.

Nat.leRecOn_self theorem

{C : ℕ → Sort*} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) : (leRecOn n.le_refl next x : C n) = x

Full source

lemma leRecOn_self {C : ℕ → Sort*} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) :
    (leRecOn n.le_refl next x : C n) = x :=
  leRec_self _ _

Base Case Preservation in Recursion Starting at $n$

Informal description

For any family of types $C(k)$ indexed by natural numbers $k$, a natural number $n$, and a function $\text{next} : \forall k, C(k) \to C(k + 1)$, the recursion term $\text{leRecOn}$ applied to the reflexive proof $n \leq n$ and an element $x \in C(n)$ satisfies: \[ \text{leRecOn}(n \leq n, \text{next}, x) = x. \]

Nat.leRecOn_succ theorem

 {C : ℕ → Sort*} {n m} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next} (x : C n) :
  (leRecOn h2 next x : C (m + 1)) = next (leRecOn h1 next x : C m)

Full source

lemma leRecOn_succ {C : ℕ → Sort*} {n m} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next} (x : C n) :
    (leRecOn h2 next x : C (m + 1)) = next (leRecOn h1 next x : C m) :=
  leRec_succ _ _ _

Recursion Step for Natural Numbers with Successor

Informal description

Let $C$ be a family of types indexed by natural numbers, and let $n$ and $m$ be natural numbers with $n \leq m$. Given: 1. A proof $h_1$ that $n \leq m$, 2. A proof $h_2$ that $n \leq m + 1$, 3. A function $\text{next} : \forall k, C(k) \to C(k + 1)$, 4. An element $x \in C(n)$, then the recursive construction satisfies: \[ \text{leRecOn}(h_2, \text{next}, x) = \text{next}(\text{leRecOn}(h_1, \text{next}, x)) \] where $\text{leRecOn}(h_2, \text{next}, x) \in C(m + 1)$ and $\text{leRecOn}(h_1, \text{next}, x) \in C(m)$.

Nat.leRecOn_succ' theorem

 {C : ℕ → Sort*} {n} {h : n ≤ n + 1} {next : ∀ {k}, C k → C (k + 1)} (x : C n) : (leRecOn h next x : C (n + 1)) = next x

Full source

lemma leRecOn_succ' {C : ℕ → Sort*} {n} {h : n ≤ n + 1} {next : ∀ {k}, C k → C (k + 1)} (x : C n) :
    (leRecOn h next x : C (n + 1)) = next x :=
  leRec_succ' _ _

Recursion Step for Successor Case Starting at Base Point $n$

Informal description

For any family of types $C(k)$ indexed by natural numbers $k$, a natural number $n$, a proof $h$ that $n \leq n + 1$, and a function $\text{next} : \forall k, C(k) \to C(k + 1)$, the recursion term $\text{leRecOn}$ applied to $h$, $\text{next}$, and an element $x \in C(n)$ satisfies: \[ \text{leRecOn}(h, \text{next}, x) = \text{next}(x). \]

Nat.leRecOn_trans theorem

 {C : ℕ → Sort*} {n m k} (hnm : n ≤ m) (hmk : m ≤ k) {next} (x : C n) :
  (leRecOn (Nat.le_trans hnm hmk) (@next) x : C k) = leRecOn hmk (@next) (leRecOn hnm (@next) x)

Full source

lemma leRecOn_trans {C : ℕ → Sort*} {n m k} (hnm : n ≤ m) (hmk : m ≤ k) {next} (x : C n) :
    (leRecOn (Nat.le_trans hnm hmk) (@next) x : C k) =
      leRecOn hmk (@next) (leRecOn hnm (@next) x) :=
  leRec_trans _ _ _ _

Transitivity of Recursive Construction on Natural Numbers

Informal description

For any family of types $C(k)$ indexed by natural numbers $k$, and natural numbers $n \leq m \leq k$, given: 1. A proof $h_{nm}$ that $n \leq m$, 2. A proof $h_{mk}$ that $m \leq k$, 3. A function $\text{next} : \forall l, C(l) \to C(l + 1)$, 4. An element $x \in C(n)$, the recursive construction satisfies: \[ \text{leRecOn}(\text{trans}(h_{nm}, h_{mk}), \text{next}, x) = \text{leRecOn}(h_{mk}, \text{next}, \text{leRecOn}(h_{nm}, \text{next}, x)) \] where $\text{trans}(h_{nm}, h_{mk})$ is the proof that $n \leq k$ obtained by transitivity from $h_{nm}$ and $h_{mk}$.

Nat.leRecOn_succ_left theorem

 {C : ℕ → Sort*} {n m} {next : ∀ {k}, C k → C (k + 1)} (x : C n) (h1 : n ≤ m) (h2 : n + 1 ≤ m) :
  (leRecOn h2 next (next x) : C m) = (leRecOn h1 next x : C m)

Full source

lemma leRecOn_succ_left {C : ℕ → Sort*} {n m}
    {next : ∀ {k}, C k → C (k + 1)} (x : C n) (h1 : n ≤ m) (h2 : n + 1 ≤ m) :
    (leRecOn h2 next (next x) : C m) = (leRecOn h1 next x : C m) :=
  leRec_succ_left (motive := fun n _ => C n) _ (fun _ _ => @next _) _ _

Recursion Equality for Successor Step in Natural Numbers

Informal description

For any family of types $C(k)$ indexed by natural numbers $k$, natural numbers $n \leq m$, and a function $\text{next} : \forall k, C(k) \to C(k + 1)$, if $x \in C(n)$ and we have both $n \leq m$ and $n + 1 \leq m$, then the recursive construction satisfies: \[ \text{leRecOn}(h_2, \text{next}, \text{next}(x)) = \text{leRecOn}(h_1, \text{next}, x) \] where $h_1$ is the proof that $n \leq m$ and $h_2$ is the proof that $n + 1 \leq m$.

Nat.strongRec' definition

{p : ℕ → Sort*} (H : ∀ n, (∀ m, m < n → p m) → p n) : ∀ n : ℕ, p n

Full source

/-- Recursion principle based on `<`. -/
@[elab_as_elim]
protected def strongRec' {p : ℕ → Sort*} (H : ∀ n, (∀ m, m < n → p m) → p n) : ∀ n : ℕ, p n
  | n => H n fun m _ ↦ Nat.strongRec' H m

Strong recursion principle for natural numbers

Informal description

Given a predicate $p$ on natural numbers and a function $H$ that for any natural number $n$ constructs a proof of $p(n)$ from proofs of $p(m)$ for all $m < n$, then $p(n)$ holds for all natural numbers $n$.

Nat.strongRecOn' definition

{P : ℕ → Sort*} (n : ℕ) (h : ∀ n, (∀ m, m < n → P m) → P n) : P n

Full source

/-- Recursion principle based on `<` applied to some natural number. -/
@[elab_as_elim]
def strongRecOn' {P : ℕ → Sort*} (n : ℕ) (h : ∀ n, (∀ m, m < n → P m) → P n) : P n :=
  Nat.strongRec' h n

Strong recursion principle for a specific natural number

Informal description

Given a predicate $P$ on natural numbers and a natural number $n$, if there exists a function $h$ that for any natural number $n$ constructs a proof of $P(n)$ from proofs of $P(m)$ for all $m < n$, then $P(n)$ holds for $n$. This is a variant of the strong recursion principle where the recursion step is applied to a specific natural number $n$.

Nat.strongRecOn'_beta theorem

{P : ℕ → Sort*} {h} : (strongRecOn' n h : P n) = h n fun m _ ↦ (strongRecOn' m h : P m)

Full source

lemma strongRecOn'_beta {P : ℕ → Sort*} {h} :
    (strongRecOn' n h : P n) = h n fun m _ ↦ (strongRecOn' m h : P m) := by
  simp only [strongRecOn']; rw [Nat.strongRec']

Recursive computation rule for strong induction on natural numbers

Informal description

For any predicate $P$ on natural numbers and any natural number $n$, the result of applying the strong recursion principle `strongRecOn'` with hypothesis $h$ at $n$ is equal to applying $h$ at $n$ with the function that maps any $m < n$ to the result of `strongRecOn'` with $h$ at $m$. In other words, the strong recursion computation satisfies the recursive equation: $$ \text{strongRecOn'}(n, h) = h(n, \lambda m \_, \text{strongRecOn'}(m, h)) $$

Nat.le_induction theorem

 {m : ℕ} {P : ∀ n, m ≤ n → Prop} (base : P m m.le_refl) (succ : ∀ n hmn, P n hmn → P (n + 1) (le_succ_of_le hmn)) :
  ∀ n hmn, P n hmn

Full source

/-- Induction principle starting at a non-zero number.
To use in an induction proof, the syntax is `induction n, hn using Nat.le_induction` (or the same
for `induction'`).

This is an alias of `Nat.leRec`, specialized to `Prop`. -/
@[elab_as_elim]
lemma le_induction {m : ℕ} {P : ∀ n, m ≤ n → Prop} (base : P m m.le_refl)
    (succ : ∀ n hmn, P n hmn → P (n + 1) (le_succ_of_le hmn)) : ∀ n hmn, P n hmn :=
  @Nat.leRec (motive := P) _ base succ

Induction Principle Starting at Non-Zero Natural Number

Informal description

Let $m$ be a natural number and $P(n, h_{mn})$ be a property depending on a natural number $n$ and a proof $h_{mn}$ that $m \leq n$. If: 1. The base case $P(m, \text{refl})$ holds (where $\text{refl}$ is the proof that $m \leq m$), and 2. For any $n \geq m$ with proof $h_{mn}$, if $P(n, h_{mn})$ holds, then $P(n+1, \text{le\_succ\_of\_le}\ h_{mn})$ holds, then $P(n, h_{mn})$ holds for all $n \geq m$ with any proof $h_{mn}$.

Nat.twoStepInduction definition

{P : ℕ → Sort*} (zero : P 0) (one : P 1) (more : ∀ n, P n → P (n + 1) → P (n + 2)) : ∀ a, P a

Full source

/-- Induction principle deriving the next case from the two previous ones. -/
def twoStepInduction {P : ℕ → Sort*} (zero : P 0) (one : P 1)
    (more : ∀ n, P n → P (n + 1) → P (n + 2)) : ∀ a, P a
  | 0 => zero
  | 1 => one
  | _ + 2 => more _ (twoStepInduction zero one more _) (twoStepInduction zero one more _)

Two-step induction principle for natural numbers

Informal description

The principle of two-step induction on natural numbers states that for any property $ P $ of natural numbers, if: 1. $ P $ holds for $ 0 $, 2. $ P $ holds for $ 1 $, and 3. For any natural number $ n $, if $ P $ holds for $ n $ and $ n + 1 $, then $ P $ holds for $ n + 2 $, then $ P $ holds for all natural numbers $ a $.

Nat.strong_induction_on theorem

{p : ℕ → Prop} (n : ℕ) (h : ∀ n, (∀ m, m < n → p m) → p n) : p n

Full source

@[elab_as_elim]
protected theorem strong_induction_on {p : ℕ → Prop} (n : ℕ)
    (h : ∀ n, (∀ m, m < n → p m) → p n) : p n :=
  Nat.strongRecOn n h

Strong Induction Principle for Natural Numbers

Informal description

For any natural number $n$ and property $p : \mathbb{N} \to \text{Prop}$, if for every $n$ we have that $p(n)$ holds whenever $p(m)$ holds for all $m < n$, then $p(n)$ holds for all $n \in \mathbb{N}$.

Nat.case_strong_induction_on theorem

{p : ℕ → Prop} (a : ℕ) (hz : p 0) (hi : ∀ n, (∀ m, m ≤ n → p m) → p (n + 1)) : p a

Full source

protected theorem case_strong_induction_on {p : ℕ → Prop} (a : ℕ) (hz : p 0)
    (hi : ∀ n, (∀ m, m ≤ n → p m) → p (n + 1)) : p a :=
  Nat.caseStrongRecOn a hz hi

Strong Induction Principle for Natural Numbers with Base Case

Informal description

For any predicate $p$ on natural numbers, to prove $p(a)$ for a natural number $a$, it suffices to: 1. Show that $p(0)$ holds (base case), and 2. For any natural number $n$, assuming $p(m)$ holds for all $m \leq n$ (strong induction hypothesis), show that $p(n+1)$ holds (inductive step).

Nat.decreasingInduction definition

 {n} {motive : (m : ℕ) → m ≤ n → Sort*} (of_succ : ∀ k (h : k < n), motive (k + 1) h → motive k (le_of_succ_le h))
  (self : motive n (Nat.le_refl _)) {m} (mn : m ≤ n) : motive m mn

Full source

/-- Decreasing induction: if `P (k+1)` implies `P k` for all `k < n`, then `P n` implies `P m` for
all `m ≤ n`.
Also works for functions to `Sort*`.

For a version also assuming `m ≤ k`, see `Nat.decreasingInduction'`. -/
@[elab_as_elim]
def decreasingInduction {n} {motive : (m : ℕ) → m ≤ n → Sort*}
    (of_succ : ∀ k (h : k < n), motive (k + 1) h → motive k (le_of_succ_le h))
    (self : motive n (Nat.le_refl _)) {m} (mn : m ≤ n) : motive m mn := by
  induction mn using leRec with
  | refl => exact self
  | @le_succ_of_le k _ ih =>
    apply ih (fun i hi => of_succ i (le_succ_of_le hi)) (of_succ k (lt_succ_self _) self)

Decreasing induction on natural numbers

Informal description

Given a natural number $n$, a family of types $C(m)$ indexed by natural numbers $m \leq n$, and: 1. A function `of_succ` that for any $k < n$ and proof $h$ that $k < n$, takes a term of $C(k+1)$ and produces a term of $C(k)$, 2. A term `self` of type $C(n)$ (the base case), the function `Nat.decreasingInduction` constructs, for any $m \leq n$ and proof $mn$ that $m \leq n$, a term of $C(m)$. This is done by recursively applying `of_succ` starting from `self`.

Nat.decreasingInduction_self theorem

 {n} {motive : (m : ℕ) → m ≤ n → Sort*} (of_succ self) :
  (decreasingInduction (motive := motive) of_succ self (Nat.le_refl _)) = self

Full source

@[simp]
lemma decreasingInduction_self {n} {motive : (m : ℕ) → m ≤ n → Sort*} (of_succ self) :
    (decreasingInduction (motive := motive) of_succ self (Nat.le_refl _)) = self := by
  dsimp only [decreasingInduction]
  rw [leRec_self]

Base Case Preservation in Decreasing Induction on Natural Numbers

Informal description

For any natural number $n$ and a family of types $C(m)$ indexed by natural numbers $m \leq n$, given: 1. A function `of_succ` that for any $k < n$ and proof $h$ that $k < n$, takes a term of $C(k+1)$ and produces a term of $C(k)$, 2. A term `self` of type $C(n)$ (the base case), the decreasing induction construction applied to the reflexive proof `Nat.le_refl n` yields the base case `self`, i.e., $$\text{decreasingInduction}(\text{of\_succ}, \text{self}, \text{Nat.le\_refl } n) = \text{self}.$$

Nat.decreasingInduction_succ theorem

 {n} {motive : (m : ℕ) → m ≤ n + 1 → Sort*} (of_succ self) (mn : m ≤ n) (msn : m ≤ n + 1) :
  (decreasingInduction (motive := motive) of_succ self msn : motive m msn) =
    decreasingInduction (motive := fun m h => motive m (le_succ_of_le h)) (fun _ _ => of_succ _ _) (of_succ _ _ self) mn

Full source

lemma decreasingInduction_succ {n} {motive : (m : ℕ) → m ≤ n + 1 → Sort*} (of_succ self)
    (mn : m ≤ n) (msn : m ≤ n + 1) :
    (decreasingInduction (motive := motive) of_succ self msn : motive m msn) =
      decreasingInduction (motive := fun m h => motive m (le_succ_of_le h))
        (fun _ _ => of_succ _ _) (of_succ _ _ self) mn := by
  dsimp only [decreasingInduction]; rw [leRec_succ]

Decreasing Induction Step Relation for Natural Numbers

Informal description

Let $n$ be a natural number and $C(m)$ be a family of types indexed by natural numbers $m \leq n+1$. Given: 1. A function `of_succ` that for any $k < n+1$ and proof $h$ that $k < n+1$, takes a term of $C(k+1)$ and produces a term of $C(k)$, 2. A term `self` of type $C(n+1)$ (the base case), 3. A natural number $m \leq n$ with proof $mn$ that $m \leq n$ and proof $msn$ that $m \leq n+1$, then the decreasing induction construction satisfies: \[ \text{decreasingInduction}(C, \text{of\_succ}, \text{self}, msn) = \text{decreasingInduction}(C', \text{of\_succ}', \text{of\_succ}(n, \text{self}), mn) \] where $C'(m, h) = C(m, \text{le\_succ\_of\_le}(h))$ and $\text{of\_succ}'(k, h) = \text{of\_succ}(k, \text{le\_succ\_of\_le}(h))$.

Nat.decreasingInduction_succ' theorem

 {n} {motive : (m : ℕ) → m ≤ n + 1 → Sort*} (of_succ self) :
  decreasingInduction (motive := motive) of_succ self n.le_succ = of_succ _ _ self

Full source

@[simp]
lemma decreasingInduction_succ' {n} {motive : (m : ℕ) → m ≤ n + 1 → Sort*} (of_succ self) :
    decreasingInduction (motive := motive) of_succ self n.le_succ = of_succ _ _ self := by
  dsimp only [decreasingInduction]; rw [leRec_succ']

Decreasing Induction Step for Successor Case at $n+1$

Informal description

For any natural number $n$ and a family of types $C(m)$ indexed by natural numbers $m \leq n+1$, given: 1. A function `of_succ` that for any $k < n+1$ and proof $h$ that $k < n+1$, takes a term of $C(k+1)$ and produces a term of $C(k)$, 2. A term `self` of type $C(n+1)$ (the base case), the decreasing induction construction satisfies: \[ \text{decreasingInduction}(C, \text{of\_succ}, \text{self}, \text{le\_succ}(n)) = \text{of\_succ}(n, \text{self}) \] where $\text{le\_succ}(n)$ is the proof that $n \leq n+1$.

Nat.decreasingInduction_trans theorem

 {motive : (m : ℕ) → m ≤ k → Sort*} (hmn : m ≤ n) (hnk : n ≤ k) (of_succ self) :
  (decreasingInduction (motive := motive) of_succ self (Nat.le_trans hmn hnk) : motive m _) =
    decreasingInduction (fun _ _ => of_succ _ _) (decreasingInduction of_succ self hnk) hmn

Full source

lemma decreasingInduction_trans {motive : (m : ℕ) → m ≤ k → Sort*} (hmn : m ≤ n) (hnk : n ≤ k)
    (of_succ self) :
    (decreasingInduction (motive := motive) of_succ self (Nat.le_trans hmn hnk) : motive m _) =
    decreasingInduction (fun _ _ => of_succ _ _) (decreasingInduction of_succ self hnk) hmn := by
  induction hnk with
  | refl => rw [decreasingInduction_self]
  | step hnk ih =>
      rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]

Transitivity of Decreasing Induction on Natural Numbers

Informal description

Let $C(m)$ be a family of types indexed by natural numbers $m \leq k$, and let: 1. `of_succ` be a function that for any $k < n$ and proof $h$ that $k < n$, takes a term of $C(k+1)$ and produces a term of $C(k)$, 2. `self` be a term of type $C(k)$ (the base case), 3. $m \leq n$ and $n \leq k$ be natural numbers with proofs $hmn$ and $hnk$ respectively. Then the decreasing induction construction satisfies: \[ \text{decreasingInduction}(C, \text{of\_succ}, \text{self}, \text{trans } hmn hnk) = \text{decreasingInduction}(C', \text{of\_succ}', \text{decreasingInduction}(C, \text{of\_succ}, \text{self}, hnk), hmn) \] where $C'(m, h) = C(m, \text{trans } h hnk)$ and $\text{of\_succ}'(k, h) = \text{of\_succ}(k, \text{trans } h hnk)$.

Nat.decreasingInduction_succ_left theorem

 {motive : (m : ℕ) → m ≤ n → Sort*} (of_succ self) (smn : m + 1 ≤ n) (mn : m ≤ n) :
  decreasingInduction (motive := motive) of_succ self mn = of_succ m smn (decreasingInduction of_succ self smn)

Full source

lemma decreasingInduction_succ_left  {motive : (m : ℕ) → m ≤ n → Sort*} (of_succ self)
    (smn : m + 1 ≤ n) (mn : m ≤ n) :
    decreasingInduction (motive := motive) of_succ self mn =
      of_succ m smn (decreasingInduction of_succ self smn) := by
  rw [Subsingleton.elim mn (Nat.le_trans (le_succ m) smn), decreasingInduction_trans,
    decreasingInduction_succ']

Decreasing Induction Step for Left Successor Case

Informal description

For any natural numbers $m$ and $n$ with $m + 1 \leq n$ and $m \leq n$, and for any family of types $C(k)$ indexed by $k \leq n$, given: 1. A function `of_succ` that for any $k < n$ and proof $h$ that $k < n$, takes a term of $C(k+1)$ and produces a term of $C(k)$, 2. A term `self` of type $C(n)$ (the base case), the decreasing induction construction satisfies: \[ \text{decreasingInduction}(C, \text{of\_succ}, \text{self}, mn) = \text{of\_succ}(m, smn, \text{decreasingInduction}(C, \text{of\_succ}, \text{self}, smn)) \] where $smn$ is the proof that $m + 1 \leq n$ and $mn$ is the proof that $m \leq n$.

Nat.strongSubRecursion definition

{P : ℕ → ℕ → Sort*} (H : ∀ m n, (∀ x y, x < m → y < n → P x y) → P m n) : ∀ n m : ℕ, P n m

Full source

/-- Given `P : ℕ → ℕ → Sort*`, if for all `m n : ℕ` we can extend `P` from the rectangle
strictly below `(m, n)` to `P m n`, then we have `P n m` for all `n m : ℕ`.
Note that for non-`Prop` output it is preferable to use the equation compiler directly if possible,
since this produces equation lemmas. -/
@[elab_as_elim]
def strongSubRecursion {P : ℕ → ℕ → Sort*} (H : ∀ m n, (∀ x y, x < m → y < n → P x y) → P m n) :
    ∀ n m : ℕ, P n m
  | n, m => H n m fun x y _ _ ↦ strongSubRecursion H x y

Strong sub-recursion principle for natural numbers

Informal description

Given a bivariate predicate $P : \mathbb{N} \times \mathbb{N} \to \text{Sort}^*$, if for all natural numbers $m$ and $n$ we can extend $P$ from all pairs $(x, y)$ with $x < m$ and $y < n$ to $P(m, n)$, then $P(n, m)$ holds for all natural numbers $n$ and $m$.

Nat.pincerRecursion definition

 {P : ℕ → ℕ → Sort*} (Ha0 : ∀ m : ℕ, P m 0) (H0b : ∀ n : ℕ, P 0 n)
  (H : ∀ x y : ℕ, P x y.succ → P x.succ y → P x.succ y.succ) : ∀ n m : ℕ, P n m

Full source

/-- Given `P : ℕ → ℕ → Sort*`, if we have `P m 0` and `P 0 n` for all `m n : ℕ`, and for any
`m n : ℕ` we can extend `P` from `(m, n + 1)` and `(m + 1, n)` to `(m + 1, n + 1)` then we have
`P m n` for all `m n : ℕ`.

Note that for non-`Prop` output it is preferable to use the equation compiler directly if possible,
since this produces equation lemmas. -/
@[elab_as_elim]
def pincerRecursion {P : ℕ → ℕ → Sort*} (Ha0 : ∀ m : ℕ, P m 0) (H0b : ∀ n : ℕ, P 0 n)
    (H : ∀ x y : ℕ, P x y.succ → P x.succ y → P x.succ y.succ) : ∀ n m : ℕ, P n m
  | m, 0 => Ha0 m
  | 0, n => H0b n
  | Nat.succ _, Nat.succ _ => H _ _ (pincerRecursion Ha0 H0b H _ _) (pincerRecursion Ha0 H0b H _ _)

Pincer recursion principle for natural numbers

Informal description

Given a two-variable predicate $P : \mathbb{N} \times \mathbb{N} \to \mathrm{Sort}^*$, if $P(m, 0)$ and $P(0, n)$ hold for all $m, n \in \mathbb{N}$, and for any $x, y \in \mathbb{N}$ we can derive $P(x+1, y+1)$ from $P(x, y+1)$ and $P(x+1, y)$, then $P(n, m)$ holds for all $n, m \in \mathbb{N}$.

Nat.decreasingInduction' definition

{P : ℕ → Sort*} (h : ∀ k < n, m ≤ k → P (k + 1) → P k) (mn : m ≤ n) (hP : P n) : P m

Full source

/-- Decreasing induction: if `P (k+1)` implies `P k` for all `m ≤ k < n`, then `P n` implies `P m`.
Also works for functions to `Sort*`.

Weakens the assumptions of `Nat.decreasingInduction`. -/
@[elab_as_elim]
def decreasingInduction' {P : ℕ → Sort*} (h : ∀ k < n, m ≤ k → P (k + 1) → P k)
    (mn : m ≤ n) (hP : P n) : P m := by
  induction mn using decreasingInduction with
  | self => exact hP
  | of_succ k hk ih =>
    exact h _ (lt_of_succ_le hk) (Nat.le_refl _)
      (ih fun k' hk' h'' => h k' hk' <| le_of_succ_le h'')

Decreasing induction principle (weak version)

Informal description

Given a predicate $P : \mathbb{N} \to \mathrm{Sort}^*$, a natural number $n$, and a proof $mn$ that $m \leq n$, if for all $k < n$ with $m \leq k$ we have that $P(k+1)$ implies $P(k)$, and if $P(n)$ holds, then $P(m)$ holds.

Nat.diag_induction theorem

 (P : ℕ → ℕ → Prop) (ha : ∀ a, P (a + 1) (a + 1)) (hb : ∀ b, P 0 (b + 1))
  (hd : ∀ a b, a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)) : ∀ a b, a < b → P a b

Full source

/-- Given a predicate on two naturals `P : ℕ → ℕ → Prop`, `P a b` is true for all `a < b` if
`P (a + 1) (a + 1)` is true for all `a`, `P 0 (b + 1)` is true for all `b` and for all
`a < b`, `P (a + 1) b` is true and `P a (b + 1)` is true implies `P (a + 1) (b + 1)` is true. -/
@[elab_as_elim]
theorem diag_induction (P : ℕ → ℕ → Prop) (ha : ∀ a, P (a + 1) (a + 1)) (hb : ∀ b, P 0 (b + 1))
    (hd : ∀ a b, a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)) : ∀ a b, a < b → P a b
  | 0, _ + 1, _ => hb _
  | a + 1, b + 1, h => by
    apply hd _ _ (Nat.add_lt_add_iff_right.1 h)
    · have this : a + 1 = b ∨ a + 1 < b := by omega
      have wf : (a + 1) + b < (a + 1) + (b + 1) := by simp
      rcases this with (rfl | h)
      · exact ha _
      apply diag_induction P ha hb hd (a + 1) b h
    have _ : a + (b + 1) < (a + 1) + (b + 1) := by simp
    apply diag_induction P ha hb hd a (b + 1)
    apply Nat.lt_of_le_of_lt (Nat.le_succ _) h

Diagonal Induction Principle for Natural Numbers

Informal description

Let $P : \mathbb{N} \times \mathbb{N} \to \mathrm{Prop}$ be a predicate on pairs of natural numbers. Suppose the following conditions hold: 1. For all $a \in \mathbb{N}$, $P(a+1, a+1)$ holds. 2. For all $b \in \mathbb{N}$, $P(0, b+1)$ holds. 3. For all $a < b$ in $\mathbb{N}$, if $P(a+1, b)$ and $P(a, b+1)$ hold, then $P(a+1, b+1)$ holds. Then for all $a < b$ in $\mathbb{N}$, $P(a, b)$ holds.

Nat.mod_two_not_eq_one theorem

: ¬n % 2 = 1 ↔ n % 2 = 0

Full source

@[simp] lemma mod_two_not_eq_one : ¬n % 2 = 1¬n % 2 = 1 ↔ n % 2 = 0 := by
  cases mod_two_eq_zero_or_one n <;> simp [*]

Parity Test: $\neg (n \mod 2 = 1) \leftrightarrow n \mod 2 = 0$

Informal description

For any natural number $n$, the remainder when $n$ is divided by 2 is not equal to 1 if and only if the remainder is equal to 0. In other words, $\neg (n \mod 2 = 1) \leftrightarrow n \mod 2 = 0$.

Nat.mod_two_not_eq_zero theorem

: ¬n % 2 = 0 ↔ n % 2 = 1

Full source

@[simp] lemma mod_two_not_eq_zero : ¬n % 2 = 0¬n % 2 = 0 ↔ n % 2 = 1 := by
  cases mod_two_eq_zero_or_one n <;> simp [*]

Characterization of Odd Natural Numbers via Modulo 2

Informal description

For any natural number $n$, the remainder when $n$ is divided by 2 is not equal to 0 if and only if it is equal to 1. In other words, $\neg (n \bmod 2 = 0) \leftrightarrow n \bmod 2 = 1$.

Nat.mod_two_ne_one theorem

: n % 2 ≠ 1 ↔ n % 2 = 0

Full source

lemma mod_two_ne_one : n % 2 ≠ 1n % 2 ≠ 1 ↔ n % 2 = 0 := mod_two_not_eq_one

Characterization of Even Natural Numbers via Modulo 2

Informal description

For any natural number $n$, the remainder when $n$ is divided by 2 is not equal to 1 if and only if it is equal to 0. In other words, $n \bmod 2 \neq 1 \leftrightarrow n \bmod 2 = 0$.

Nat.mod_two_ne_zero theorem

: n % 2 ≠ 0 ↔ n % 2 = 1

Full source

lemma mod_two_ne_zero : n % 2 ≠ 0n % 2 ≠ 0 ↔ n % 2 = 1 := mod_two_not_eq_zero

Characterization of Nonzero Remainder Modulo 2: $n \bmod 2 \neq 0 \leftrightarrow n \bmod 2 = 1$

Informal description

For any natural number $n$, the remainder when $n$ is divided by 2 is not equal to 0 if and only if it is equal to 1. In other words, $n \bmod 2 \neq 0 \leftrightarrow n \bmod 2 = 1$.

Nat.lt_div_iff_mul_lt' theorem

(hdn : d ∣ n) (a : ℕ) : a < n / d ↔ d * a < n

Full source

/-- Variant of `Nat.lt_div_iff_mul_lt` that assumes `d ∣ n`. -/
protected lemma lt_div_iff_mul_lt' (hdn : d ∣ n) (a : ℕ) : a < n / d ↔ d * a < n := by
  obtain rfl | hd := d.eq_zero_or_pos
  · simp [Nat.zero_dvd.1 hdn]
  · rw [← Nat.mul_lt_mul_left hd, ← Nat.eq_mul_of_div_eq_right hdn rfl]

Division Inequality under Divisibility: $a < n/d \leftrightarrow d \cdot a < n$ when $d \mid n$

Informal description

For natural numbers $d$ and $n$ such that $d$ divides $n$, and for any natural number $a$, we have $a < n / d$ if and only if $d \cdot a < n$.

Nat.mul_div_eq_iff_dvd theorem

{n d : ℕ} : d * (n / d) = n ↔ d ∣ n

Full source

lemma mul_div_eq_iff_dvd {n d : ℕ} : d * (n / d) = n ↔ d ∣ n :=
  calc
    d * (n / d) = n ↔ d * (n / d) = d * (n / d) + (n % d) := by rw [div_add_mod]
    _ ↔ d ∣ n := by rw [eq_comm, Nat.add_eq_left, dvd_iff_mod_eq_zero]

Division-Multiplication Equality Characterizes Divisibility in Natural Numbers

Informal description

For natural numbers $d$ and $n$, the equality $d \cdot (n / d) = n$ holds if and only if $d$ divides $n$.

Nat.mul_div_lt_iff_not_dvd theorem

: d * (n / d) < n ↔ ¬d ∣ n

Full source

lemma mul_div_lt_iff_not_dvd : d * (n / d) < n ↔ ¬ d ∣ n := by
  simp [Nat.lt_iff_le_and_ne, mul_div_eq_iff_dvd, mul_div_le]

Inequality of Division and Multiplication Characterizes Non-Divisibility in Natural Numbers

Informal description

For natural numbers $d$ and $n$, the inequality $d \cdot (n / d) < n$ holds if and only if $d$ does not divide $n$.

Nat.div_eq_iff_eq_of_dvd_dvd theorem

(hn : n ≠ 0) (ha : a ∣ n) (hb : b ∣ n) : n / a = n / b ↔ a = b

Full source

lemma div_eq_iff_eq_of_dvd_dvd (hn : n ≠ 0) (ha : a ∣ n) (hb : b ∣ n) : n / a = n / b ↔ a = b := by
  constructor <;> intro h
  · rw [← Nat.mul_right_inj hn]
    apply Nat.eq_mul_of_div_eq_left (Nat.dvd_trans hb (Nat.dvd_mul_right _ _))
    rw [eq_comm, Nat.mul_comm, Nat.mul_div_assoc _ hb]
    exact Nat.eq_mul_of_div_eq_right ha h
  · rw [h]

Division Equality Condition for Divisors of a Nonzero Natural Number

Informal description

For any nonzero natural number $n$ and natural numbers $a$ and $b$ such that both $a$ and $b$ divide $n$, the equality $n / a = n / b$ holds if and only if $a = b$.

Nat.le_iff_ne_zero_of_dvd theorem

(ha : a ≠ 0) (hab : a ∣ b) : a ≤ b ↔ b ≠ 0

Full source

lemma le_iff_ne_zero_of_dvd (ha : a ≠ 0) (hab : a ∣ b) : a ≤ b ↔ b ≠ 0 where
  mp := by rw [← Nat.pos_iff_ne_zero] at ha ⊢; exact Nat.lt_of_lt_of_le ha
  mpr hb := Nat.le_of_dvd (Nat.pos_iff_ne_zero.2 hb) hab

Nonzero Divisor Implies Nonzero Dividend and Inequality

Informal description

For any nonzero natural numbers $a$ and $b$ such that $a$ divides $b$, the inequality $a \leq b$ holds if and only if $b$ is nonzero.

Nat.div_ne_zero_iff_of_dvd theorem

(hba : b ∣ a) : a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

Full source

lemma div_ne_zero_iff_of_dvd (hba : b ∣ a) : a / b ≠ 0a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by
  obtain rfl | hb := Decidable.em (b = 0) <;>
    simp [Nat.div_ne_zero_iff, Nat.le_iff_ne_zero_of_dvd, *]

Nonzero Division Condition for Natural Numbers under Divisibility

Informal description

For natural numbers $a$ and $b$ such that $b$ divides $a$, the division $a / b$ is nonzero if and only if both $a$ and $b$ are nonzero.

Nat.pow_mod theorem

(a b n : ℕ) : a ^ b % n = (a % n) ^ b % n

Full source

lemma pow_mod (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n := by
  induction b with
  | zero => rfl
  | succ b ih => simp [Nat.pow_succ, Nat.mul_mod, ih]

Modular Exponentiation Property: $a^b \bmod n = (a \bmod n)^b \bmod n$

Informal description

For any natural numbers $a$, $b$, and $n$, the remainder when $a^b$ is divided by $n$ is equal to the remainder when $(a \bmod n)^b$ is divided by $n$, i.e., $$a^b \bmod n = (a \bmod n)^b \bmod n.$$

Nat.not_pos_pow_dvd theorem

: ∀ {a n : ℕ} (_ : 1 < a) (_ : 1 < n), ¬a ^ n ∣ a

Full source

lemma not_pos_pow_dvd : ∀ {a n : ℕ} (_ : 1 < a) (_ : 1 < n), ¬ a ^ n ∣ a
  | succ a, succ n, hp, hk, h =>
    have : succ a * succ a ^ n ∣ succ a * 1 := by simpa [pow_succ'] using h
    have : succ a ^ n ∣ 1 := Nat.dvd_of_mul_dvd_mul_left (succ_pos _) this
    have he : succ a ^ n = 1 := eq_one_of_dvd_one this
    have : n < succ a ^ n := n.lt_pow_self hp
    have : n < 1 := by rwa [he] at this
    have : n = 0 := Nat.eq_zero_of_le_zero <| le_of_lt_succ this
    have : 1 < 1 := by rwa [this] at hk
    absurd this (by decide)

Non-divisibility of a by its own power for $a > 1$ and $n > 1$

Informal description

For any natural numbers $a$ and $n$ such that $1 < a$ and $1 < n$, the power $a^n$ does not divide $a$.

Nat.lt_of_pow_dvd_right theorem

(hb : b ≠ 0) (ha : 2 ≤ a) (h : a ^ n ∣ b) : n < b

Full source

lemma lt_of_pow_dvd_right (hb : b ≠ 0) (ha : 2 ≤ a) (h : a ^ n ∣ b) : n < b := by
  rw [← Nat.pow_lt_pow_iff_right (succ_le_iff.1 ha)]
  exact Nat.lt_of_le_of_lt (le_of_dvd (Nat.pos_iff_ne_zero.2 hb) h) (Nat.lt_pow_self ha)

Upper Bound on Exponent in Power Divisibility: $a^n \mid b \Rightarrow n < b$ for $a \geq 2$ and $b \neq 0$

Informal description

For any natural numbers $a$, $b$, and $n$, if $b \neq 0$, $a \geq 2$, and $a^n$ divides $b$, then $n < b$.

Nat.div_dvd_of_dvd theorem

(h : n ∣ m) : m / n ∣ m

Full source

lemma div_dvd_of_dvd (h : n ∣ m) : m / n ∣ m := ⟨n, (Nat.div_mul_cancel h).symm⟩

Divisibility of Quotient: $n \mid m \Rightarrow (m/n) \mid m$

Informal description

For any natural numbers $n$ and $m$ such that $n$ divides $m$, the quotient $m/n$ also divides $m$.

Nat.div_div_self theorem

(h : n ∣ m) (hm : m ≠ 0) : m / (m / n) = n

Full source

protected lemma div_div_self (h : n ∣ m) (hm : m ≠ 0) : m / (m / n) = n := by
  rcases h with ⟨_, rfl⟩
  rw [Nat.mul_ne_zero_iff] at hm
  rw [mul_div_right _ (Nat.pos_of_ne_zero hm.1), mul_div_left _ (Nat.pos_of_ne_zero hm.2)]

Division Cancellation: $m / (m / n) = n$ when $n \mid m$ and $m \neq 0$

Informal description

For any natural numbers $n$ and $m$ such that $n$ divides $m$ and $m \neq 0$, we have $m / (m / n) = n$.

Nat.not_dvd_of_pos_of_lt theorem

(h1 : 0 < n) (h2 : n < m) : ¬m ∣ n

Full source

lemma not_dvd_of_pos_of_lt (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n := by
  rintro ⟨k, rfl⟩
  rcases Nat.eq_zero_or_pos k with (rfl | hk)
  · exact Nat.lt_irrefl 0 h1
  · exact Nat.not_lt.2 (Nat.le_mul_of_pos_right _ hk) h2

Non-divisibility of Smaller Positive Natural Numbers

Informal description

For any positive natural numbers $n$ and $m$ such that $n < m$, it holds that $m$ does not divide $n$.

Nat.mod_eq_iff_lt theorem

(hn : n ≠ 0) : m % n = m ↔ m < n

Full source

lemma mod_eq_iff_lt (hn : n ≠ 0) : m % n = m ↔ m < n :=
  ⟨fun h ↦ by rw [← h]; exact mod_lt _ <| Nat.pos_iff_ne_zero.2 hn, mod_eq_of_lt⟩

Remainder Equals Dividend if and only if Dividend is Less Than Divisor

Informal description

For any natural numbers $m$ and $n$ with $n \neq 0$, the remainder of $m$ divided by $n$ equals $m$ if and only if $m$ is strictly less than $n$. In other words, $m \% n = m \leftrightarrow m < n$.

Nat.mod_succ_eq_iff_lt theorem

: m % n.succ = m ↔ m < n.succ

Full source

@[simp]
lemma mod_succ_eq_iff_lt : m % n.succ = m ↔ m < n.succ :=
  mod_eq_iff_lt (succ_ne_zero _)

Remainder Equals Dividend Modulo Successor if and only if Dividend is Less Than Successor

Informal description

For any natural numbers $m$ and $n$, the remainder of $m$ divided by $n+1$ equals $m$ if and only if $m$ is strictly less than $n+1$. In other words, $m \bmod (n + 1) = m \leftrightarrow m < n + 1$.

Nat.mod_succ theorem

(n : ℕ) : n % n.succ = n

Full source

@[simp] lemma mod_succ (n : ℕ) : n % n.succ = n := mod_eq_of_lt n.lt_succ_self

Remainder Identity: $n \bmod (n + 1) = n$

Informal description

For any natural number $n$, the remainder when $n$ is divided by $n + 1$ is equal to $n$ itself, i.e., $n \bmod (n + 1) = n$.

Nat.mod_add_div' theorem

(a b : ℕ) : a % b + a / b * b = a

Full source

lemma mod_add_div' (a b : ℕ) : a % b + a / b * b = a := by rw [Nat.mul_comm]; exact mod_add_div _ _

Division Algorithm for Natural Numbers: $a \% b + (a / b) \cdot b = a$

Informal description

For any natural numbers $a$ and $b$, the sum of the remainder $a \% b$ and the product of the quotient $a / b$ with $b$ equals $a$, i.e., $a \% b + (a / b) \cdot b = a$.

Nat.div_add_mod' theorem

(a b : ℕ) : a / b * b + a % b = a

Full source

lemma div_add_mod' (a b : ℕ) : a / b * b + a % b = a := by rw [Nat.mul_comm]; exact div_add_mod _ _

Division-Remainder Decomposition for Natural Numbers

Informal description

For any natural numbers $a$ and $b$, the sum of the product of the integer division $a / b$ with $b$ and the remainder $a \% b$ equals $a$, i.e., $(a / b) \cdot b + (a \% b) = a$.

Nat.div_mod_unique theorem

(h : 0 < b) : a / b = d ∧ a % b = c ↔ c + b * d = a ∧ c < b

Full source

/-- See also `Nat.divModEquiv` for a similar statement as an `Equiv`. -/
protected lemma div_mod_unique (h : 0 < b) :
    a / b = d ∧ a % b = ca / b = d ∧ a % b = c ↔ c + b * d = a ∧ c < b :=
  ⟨fun ⟨e₁, e₂⟩ ↦ e₁ ▸ e₂ ▸ ⟨mod_add_div _ _, mod_lt _ h⟩, fun ⟨h₁, h₂⟩ ↦ h₁ ▸ by
    rw [add_mul_div_left _ _ h, add_mul_mod_self_left]; simp [div_eq_of_lt, mod_eq_of_lt, h₂]⟩

Characterization of Division and Remainder in Natural Numbers

Informal description

For natural numbers $a$, $b$, $c$, and $d$ with $b > 0$, the following are equivalent: 1. The quotient of $a$ divided by $b$ is $d$ and the remainder is $c$. 2. The equation $c + b \cdot d = a$ holds and $c < b$.

Nat.sub_mod_eq_zero_of_mod_eq theorem

(h : m % k = n % k) : (m - n) % k = 0

Full source

/-- If `m` and `n` are equal mod `k`, `m - n` is zero mod `k`. -/
lemma sub_mod_eq_zero_of_mod_eq (h : m % k = n % k) : (m - n) % k = 0 := by
  rw [← Nat.mod_add_div m k, ← Nat.mod_add_div n k, ← h, ← Nat.sub_sub,
    Nat.add_sub_cancel_left, ← k.mul_sub, Nat.mul_mod_right]

Difference of Congruent Numbers is Divisible

Informal description

For any natural numbers $m$, $n$, and $k$, if $m \equiv n \pmod{k}$, then $(m - n) \equiv 0 \pmod{k}$.

Nat.one_mod theorem

(n : ℕ) : 1 % (n + 2) = 1

Full source

@[simp] lemma one_mod (n : ℕ) : 1 % (n + 2) = 1 :=
  Nat.mod_eq_of_lt (Nat.add_lt_add_right n.succ_pos 1)

Modulo Identity: $1 \mod (n + 2) = 1$

Informal description

For any natural number $n$, the remainder when $1$ is divided by $n + 2$ is $1$, i.e., $1 \mod (n + 2) = 1$.

Nat.one_mod_eq_one theorem

: ∀ {n : ℕ}, 1 % n = 1 ↔ n ≠ 1

Full source

lemma one_mod_eq_one : ∀ {n : ℕ}, 1 % n = 1 ↔ n ≠ 1
  | 0 | 1 | n + 2 => by simp

Modulo Identity: $1 \mod n = 1 \leftrightarrow n \neq 1$

Informal description

For any natural number $n$, the remainder when $1$ is divided by $n$ equals $1$ if and only if $n \neq 1$. In other words, $1 \mod n = 1 \leftrightarrow n \neq 1$.

Nat.dvd_sub_mod theorem

(k : ℕ) : n ∣ k - k % n

Full source

lemma dvd_sub_mod (k : ℕ) : n ∣ k - k % n :=
  ⟨k / n, Nat.sub_eq_of_eq_add (Nat.div_add_mod k n).symm⟩

Divisibility of Difference by Modulus: $n \mid (k - k \% n)$

Informal description

For any natural numbers $n$ and $k$, $n$ divides the difference between $k$ and the remainder when $k$ is divided by $n$, i.e., $n \mid (k - k \% n)$.

Nat.add_mod_eq_ite theorem

: (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k

Full source

lemma add_mod_eq_ite :
    (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k := by
  cases k with
  | zero => simp
  | succ k =>
    rw [Nat.add_mod]
    by_cases h : k + 1 ≤ m % (k + 1) + n % (k + 1)
    · rw [if_pos h, Nat.mod_eq_sub_mod h, Nat.mod_eq_of_lt]
      exact (Nat.sub_lt_iff_lt_add' h).mpr (Nat.add_lt_add (m.mod_lt (zero_lt_succ _))
        (n.mod_lt (zero_lt_succ _)))
    · rw [if_neg h]
      exact Nat.mod_eq_of_lt (Nat.lt_of_not_ge h)

Modular Addition Formula: $(m + n) \% k$ as Conditional Expression

Informal description

For any natural numbers $m$, $n$, and $k$, the remainder of $(m + n)$ modulo $k$ is given by: \[ (m + n) \% k = \begin{cases} (m \% k + n \% k) - k & \text{if } k \leq m \% k + n \% k, \\ m \% k + n \% k & \text{otherwise.} \end{cases} \]

Nat.not_dvd_of_between_consec_multiples theorem

(h1 : n * k < m) (h2 : m < n * (k + 1)) : ¬n ∣ m

Full source

/-- `m` is not divisible by `n` if it is between `n * k` and `n * (k + 1)` for some `k`. -/
theorem not_dvd_of_between_consec_multiples (h1 : n * k < m) (h2 : m < n * (k + 1)) : ¬n ∣ m := by
  rintro ⟨d, rfl⟩
  have := Nat.lt_of_mul_lt_mul_left h1
  have := Nat.lt_of_mul_lt_mul_left h2
  omega

Non-divisibility between consecutive multiples: $n \nmid m$ when $n \cdot k < m < n \cdot (k + 1)$

Informal description

For any natural numbers $n$, $m$, and $k$, if $m$ satisfies $n \cdot k < m < n \cdot (k + 1)$, then $n$ does not divide $m$.

Nat.dvd_add_left theorem

(h : a ∣ c) : a ∣ b + c ↔ a ∣ b

Full source

protected lemma dvd_add_left (h : a ∣ c) : a ∣ b + ca ∣ b + c ↔ a ∣ b := (Nat.dvd_add_iff_left h).symm

Divisibility of Sum When One Term is Divisible: $a \mid b + c \leftrightarrow a \mid b$ given $a \mid c$

Informal description

For any natural numbers $a$, $b$, and $c$, if $a$ divides $c$, then $a$ divides $b + c$ if and only if $a$ divides $b$.

Nat.dvd_add_right theorem

(h : a ∣ b) : a ∣ b + c ↔ a ∣ c

Full source

protected lemma dvd_add_right (h : a ∣ b) : a ∣ b + ca ∣ b + c ↔ a ∣ c := (Nat.dvd_add_iff_right h).symm

Divisibility of Sum by Divisor of One Term: $a \mid b \Rightarrow (a \mid b + c \leftrightarrow a \mid c)$

Informal description

For any natural numbers $a$, $b$, and $c$, if $a$ divides $b$, then $a$ divides $b + c$ if and only if $a$ divides $c$.

Nat.mul_dvd_mul_iff_left theorem

(ha : 0 < a) : a * b ∣ a * c ↔ b ∣ c

Full source

/-- special case of `mul_dvd_mul_iff_left` for `ℕ`.
Duplicated here to keep simple imports for this file. -/
protected lemma mul_dvd_mul_iff_left (ha : 0 < a) : a * b ∣ a * ca * b ∣ a * c ↔ b ∣ c :=
  exists_congr fun d ↦ by rw [Nat.mul_assoc, Nat.mul_right_inj <| ne_of_gt ha]

Left Cancellation Law for Divisibility of Natural Numbers: $a > 0 \Rightarrow (a \cdot b \mid a \cdot c \leftrightarrow b \mid c)$

Informal description

For any natural numbers $a$, $b$, and $c$ with $a > 0$, the product $a \cdot b$ divides $a \cdot c$ if and only if $b$ divides $c$.

Nat.mul_dvd_mul_iff_right theorem

(hc : 0 < c) : a * c ∣ b * c ↔ a ∣ b

Full source

/-- special case of `mul_dvd_mul_iff_right` for `ℕ`.
Duplicated here to keep simple imports for this file. -/
protected lemma mul_dvd_mul_iff_right (hc : 0 < c) : a * c ∣ b * ca * c ∣ b * c ↔ a ∣ b :=
  exists_congr fun d ↦ by rw [Nat.mul_right_comm, Nat.mul_left_inj <| ne_of_gt hc]

Right Cancellation Law for Divisibility in Natural Numbers: $a \cdot c \mid b \cdot c \leftrightarrow a \mid b$ for $c > 0$

Informal description

For any natural numbers $a$, $b$, and $c$ with $c > 0$, the product $a \cdot c$ divides $b \cdot c$ if and only if $a$ divides $b$.

Nat.add_mod_eq_add_mod_right theorem

(c : ℕ) (H : a % d = b % d) : (a + c) % d = (b + c) % d

Full source

lemma add_mod_eq_add_mod_right (c : ℕ) (H : a % d = b % d) : (a + c) % d = (b + c) % d := by
  rw [← mod_add_mod, ← mod_add_mod b, H]

Modular Arithmetic: Right Addition Preserves Congruence

Informal description

For any natural numbers $a$, $b$, $c$, and $d$, if $a \bmod d = b \bmod d$, then $(a + c) \bmod d = (b + c) \bmod d$.

Nat.add_mod_eq_add_mod_left theorem

(c : ℕ) (H : a % d = b % d) : (c + a) % d = (c + b) % d

Full source

lemma add_mod_eq_add_mod_left (c : ℕ) (H : a % d = b % d) : (c + a) % d = (c + b) % d := by
  rw [Nat.add_comm, add_mod_eq_add_mod_right _ H, Nat.add_comm]

Modular Arithmetic: Left Addition Preserves Congruence

Informal description

For any natural numbers $a$, $b$, $c$, and $d$, if $a \bmod d = b \bmod d$, then $(c + a) \bmod d = (c + b) \bmod d$.

Nat.mul_dvd_of_dvd_div theorem

(hcb : c ∣ b) (h : a ∣ b / c) : c * a ∣ b

Full source

lemma mul_dvd_of_dvd_div (hcb : c ∣ b) (h : a ∣ b / c) : c * a ∣ b :=
  have ⟨d, hd⟩ := h
  ⟨d, by simpa [Nat.mul_comm, Nat.mul_left_comm] using Nat.eq_mul_of_div_eq_left hcb hd⟩

Product Divisibility from Quotient Divisibility

Informal description

For any natural numbers $a$, $b$, and $c$, if $c$ divides $b$ and $a$ divides the quotient $b / c$, then the product $c \cdot a$ divides $b$.

Nat.div_le_div theorem

{a b c d : ℕ} (h1 : a ≤ b) (h2 : d ≤ c) (h3 : d ≠ 0) : a / c ≤ b / d

Full source

protected theorem div_le_div {a b c d : ℕ} (h1 : a ≤ b) (h2 : d ≤ c) (h3 : d ≠ 0) : a / c ≤ b / d :=
  calc a / c ≤ b / c := Nat.div_le_div_right h1
    _ ≤ b / d := Nat.div_le_div_left h2 (Nat.pos_of_ne_zero h3)

Monotonicity of Natural Division: $\frac{a}{c} \leq \frac{b}{d}$ under $a \leq b$ and $d \leq c$

Informal description

For any natural numbers $a, b, c, d$ such that $a \leq b$, $d \leq c$, and $d \neq 0$, we have the inequality: $$\frac{a}{c} \leq \frac{b}{d}.$$

Nat.lt_mul_div_succ theorem

(a : ℕ) (hb : 0 < b) : a < b * (a / b + 1)

Full source

lemma lt_mul_div_succ (a : ℕ) (hb : 0 < b) : a < b * (a / b + 1) := by
  rw [Nat.mul_comm, ← Nat.div_lt_iff_lt_mul hb]
  exact lt_succ_self _

Upper bound on natural division: $a < b(\lfloor a/b \rfloor + 1)$

Informal description

For any natural numbers $a$ and $b$ with $b > 0$, we have the inequality $a < b \cdot (\lfloor a/b \rfloor + 1)$.

Nat.mul_add_mod' theorem

(a b c : ℕ) : (a * b + c) % b = c % b

Full source

lemma mul_add_mod' (a b c : ℕ) : (a * b + c) % b = c % b := by rw [Nat.mul_comm, Nat.mul_add_mod]

Modular Arithmetic Identity: $(ab + c) \bmod b = c \bmod b$

Informal description

For any natural numbers $a$, $b$, and $c$, the remainder of $(a \cdot b + c)$ when divided by $b$ is equal to the remainder of $c$ when divided by $b$, i.e., $$(a \cdot b + c) \bmod b = c \bmod b.$$

Nat.mul_add_mod_of_lt theorem

(h : c < b) : (a * b + c) % b = c

Full source

lemma mul_add_mod_of_lt (h : c < b) : (a * b + c) % b = c := by
  rw [Nat.mul_add_mod', Nat.mod_eq_of_lt h]

Modular Reduction Identity for $c < b$: $(ab + c) \bmod b = c$

Informal description

For any natural numbers $a$, $b$, and $c$ with $c < b$, the remainder of $(a \cdot b + c)$ when divided by $b$ is equal to $c$, i.e., $$(a \cdot b + c) \bmod b = c.$$

Nat.not_two_dvd_bit1 theorem

(n : ℕ) : ¬2 ∣ 2 * n + 1

Full source

@[simp]
protected theorem not_two_dvd_bit1 (n : ℕ) : ¬2 ∣ 2 * n + 1 := by
  omega

Odd numbers are not divisible by 2

Informal description

For any natural number $n$, the number $2n + 1$ is not divisible by 2.

Nat.dvd_add_self_left theorem

: m ∣ m + n ↔ m ∣ n

Full source

/-- A natural number `m` divides the sum `m + n` if and only if `m` divides `n`. -/
@[simp] protected lemma dvd_add_self_left : m ∣ m + nm ∣ m + n ↔ m ∣ n := Nat.dvd_add_right (Nat.dvd_refl m)

Divisibility of Sum by First Term: $m \mid (m + n) \leftrightarrow m \mid n$

Informal description

For any natural numbers $m$ and $n$, $m$ divides $m + n$ if and only if $m$ divides $n$.

Nat.dvd_add_self_right theorem

: m ∣ n + m ↔ m ∣ n

Full source

/-- A natural number `m` divides the sum `n + m` if and only if `m` divides `n`. -/
@[simp] protected lemma dvd_add_self_right : m ∣ n + mm ∣ n + m ↔ m ∣ n := Nat.dvd_add_left (Nat.dvd_refl m)

Divisibility of Sum by Term: $m \mid n + m \leftrightarrow m \mid n$

Informal description

For any natural numbers $m$ and $n$, $m$ divides $n + m$ if and only if $m$ divides $n$.

Nat.dvd_iff_div_mul_eq theorem

(n d : ℕ) : d ∣ n ↔ n / d * d = n

Full source

lemma dvd_iff_div_mul_eq (n d : ℕ) : d ∣ nd ∣ n ↔ n / d * d = n :=
  ⟨fun h => Nat.div_mul_cancel h, fun h => by rw [← h]; exact Nat.dvd_mul_left _ _⟩

Divisibility Criterion via Division and Multiplication

Informal description

For any natural numbers $n$ and $d$, $d$ divides $n$ if and only if the product of $n$ divided by $d$ and $d$ equals $n$, i.e., $d \mid n \leftrightarrow (n / d) \times d = n$.

Nat.dvd_iff_le_div_mul theorem

(n d : ℕ) : d ∣ n ↔ n ≤ n / d * d

Full source

lemma dvd_iff_le_div_mul (n d : ℕ) : d ∣ nd ∣ n ↔ n ≤ n / d * d :=
  ((dvd_iff_div_mul_eq _ _).trans Nat.le_antisymm_iff).trans (and_iff_right (div_mul_le_self n d))

Divisibility Criterion via Inequality of Division and Multiplication

Informal description

For any natural numbers $n$ and $d$, $d$ divides $n$ if and only if $n$ is less than or equal to the product of $n$ divided by $d$ and $d$, i.e., $d \mid n \leftrightarrow n \leq (n / d) \times d$.

Nat.dvd_iff_dvd_dvd theorem

(n d : ℕ) : d ∣ n ↔ ∀ k : ℕ, k ∣ d → k ∣ n

Full source

lemma dvd_iff_dvd_dvd (n d : ℕ) : d ∣ nd ∣ n ↔ ∀ k : ℕ, k ∣ d → k ∣ n :=
  ⟨fun h _ hkd => Nat.dvd_trans hkd h, fun h => h _ (Nat.dvd_refl _)⟩

Divisibility Characterization: $d \mid n \leftrightarrow (\forall k, k \mid d \to k \mid n)$

Informal description

For any natural numbers $n$ and $d$, $d$ divides $n$ if and only if every natural number $k$ that divides $d$ also divides $n$.

Nat.dvd_div_of_mul_dvd theorem

(h : a * b ∣ c) : b ∣ c / a

Full source

lemma dvd_div_of_mul_dvd (h : a * b ∣ c) : b ∣ c / a :=
  if ha : a = 0 then by simp [ha]
  else
    have ha : 0 < a := Nat.pos_of_ne_zero ha
    have h1 : ∃ d, c = a * b * d := h
    let ⟨d, hd⟩ := h1
    have h2 : c / a = b * d := Nat.div_eq_of_eq_mul_right ha (by simpa [Nat.mul_assoc] using hd)
    show ∃ d, c / a = b * d from ⟨d, h2⟩

Divisibility of Quotient by Factor in Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$, if $a \times b$ divides $c$, then $b$ divides the quotient $c / a$.

Nat.dvd_div_iff_mul_dvd theorem

(hbc : c ∣ b) : a ∣ b / c ↔ c * a ∣ b

Full source

@[simp] lemma dvd_div_iff_mul_dvd (hbc : c ∣ b) : a ∣ b / ca ∣ b / c ↔ c * a ∣ b :=
  ⟨fun h => mul_dvd_of_dvd_div hbc h, fun h => dvd_div_of_mul_dvd h⟩

Divisibility Equivalence: $a \mid (b/c) \leftrightarrow c \cdot a \mid b$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $c$ divides $b$, we have that $a$ divides $b/c$ if and only if $c \cdot a$ divides $b$.

Nat.dvd_mul_of_div_dvd theorem

(h : b ∣ a) (hdiv : a / b ∣ c) : a ∣ b * c

Full source

lemma dvd_mul_of_div_dvd (h : b ∣ a) (hdiv : a / b ∣ c) : a ∣ b * c := by
  obtain ⟨e, rfl⟩ := hdiv
  rw [← Nat.mul_assoc, Nat.mul_comm _ (a / b), Nat.div_mul_cancel h]
  exact Nat.dvd_mul_right a e

Divisibility of Product by Divisor of Quotient

Informal description

For any natural numbers $a$, $b$, and $c$, if $b$ divides $a$ and $a/b$ divides $c$, then $a$ divides $b \cdot c$.

Nat.div_dvd_iff_dvd_mul theorem

(h : b ∣ a) (hb : b ≠ 0) : a / b ∣ c ↔ a ∣ b * c

Full source

@[simp] lemma div_dvd_iff_dvd_mul (h : b ∣ a) (hb : b ≠ 0) : a / b ∣ ca / b ∣ c ↔ a ∣ b * c :=
  exists_congr <| fun d => by
  have := Nat.dvd_trans (Nat.dvd_mul_left _ d) (Nat.mul_dvd_mul_left d h)
  rw [eq_comm, Nat.mul_comm, ← Nat.mul_div_assoc d h,
    Nat.div_eq_iff_eq_mul_right (Nat.pos_of_ne_zero hb) this, Nat.mul_comm, eq_comm]

Divisibility of Quotient Implies Divisibility of Product in Natural Numbers

Informal description

For natural numbers $a$, $b$, and $c$ with $b \neq 0$, if $b$ divides $a$, then $a/b$ divides $c$ if and only if $a$ divides $b \cdot c$.

Nat.div_div_div_eq_div theorem

(dvd : b ∣ a) (dvd2 : a ∣ c) : c / (a / b) / b = c / a

Full source

@[simp] lemma div_div_div_eq_div (dvd : b ∣ a) (dvd2 : a ∣ c) : c / (a / b) / b = c / a :=
  match a, b, c with
  | 0, _, _ => by simp
  | a + 1, 0, _ => by simp at dvd
  | a + 1, c + 1, _ => by
    have a_split : a + 1 ≠ 0 := succ_ne_zero a
    have c_split : c + 1 ≠ 0 := succ_ne_zero c
    rcases dvd2 with ⟨k, rfl⟩
    rcases dvd with ⟨k2, pr⟩
    have k2_nonzero : k2 ≠ 0 := fun k2_zero => by simp [k2_zero] at pr
    rw [Nat.mul_div_cancel_left k (Nat.pos_of_ne_zero a_split), pr,
      Nat.mul_div_cancel_left k2 (Nat.pos_of_ne_zero c_split), Nat.mul_comm ((c + 1) * k2) k, ←
      Nat.mul_assoc k (c + 1) k2, Nat.mul_div_cancel _ (Nat.pos_of_ne_zero k2_nonzero),
      Nat.mul_div_cancel _ (Nat.pos_of_ne_zero c_split)]

Triple Division Identity for Natural Numbers under Divisibility Conditions

Informal description

For any natural numbers $a$, $b$, and $c$ such that $b$ divides $a$ and $a$ divides $c$, the following equality holds: \[ \frac{c / (a / b)}{b} = \frac{c}{a}. \]

Nat.le_of_lt_add_of_dvd theorem

(h : a < b + n) : n ∣ a → n ∣ b → a ≤ b

Full source

lemma le_of_lt_add_of_dvd (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b := by
  rintro ⟨a, rfl⟩ ⟨b, rfl⟩
  rw [← mul_succ] at h
  exact Nat.mul_le_mul_left _ (Nat.lt_succ_iff.1 <| Nat.lt_of_mul_lt_mul_left h)

Comparison of Natural Numbers Under Divisibility and Addition Constraint

Informal description

For natural numbers $a$, $b$, and $n$, if $a < b + n$ and $n$ divides both $a$ and $b$, then $a \leq b$.

Nat.not_dvd_iff_lt_mul_succ theorem

(n : ℕ) {a : ℕ} (ha : 0 < a) : ¬a ∣ n ↔ (∃ k : ℕ, a * k < n ∧ n < a * (k + 1))

Full source

lemma not_dvd_iff_lt_mul_succ (n : ℕ) {a : ℕ} (ha : 0 < a) :
     ¬ a ∣ n¬ a ∣ n ↔ (∃ k : ℕ, a * k < n ∧ n < a * (k + 1)) := by
  refine
    ⟨fun han =>
      ⟨n / a, ⟨Nat.lt_of_le_of_ne (mul_div_le n a) ?_, lt_mul_div_succ _ ha⟩⟩,
      fun ⟨k, hk1, hk2⟩ => not_dvd_of_between_consec_multiples hk1 hk2⟩
  exact mt (⟨n / a, Eq.symm ·⟩) han

Non-divisibility criterion via consecutive multiples: $\neg(a \mid n) \leftrightarrow \exists k, a \cdot k < n < a \cdot (k + 1)$

Informal description

For any natural numbers $n$ and $a$ with $a > 0$, the statement that $a$ does not divide $n$ is equivalent to the existence of a natural number $k$ such that $a \cdot k < n < a \cdot (k + 1)$.

Nat.not_dvd_iff_between_consec_multiples theorem

(n : ℕ) {a : ℕ} (ha : 0 < a) : ¬a ∣ n ↔ (∃ k : ℕ, a * k < n ∧ n < a * (k + 1))

Full source

/-- `n` is not divisible by `a` iff it is between `a * k` and `a * (k + 1)` for some `k`. -/
lemma not_dvd_iff_between_consec_multiples (n : ℕ) {a : ℕ} (ha : 0 < a) :
    ¬ a ∣ n¬ a ∣ n ↔ (∃ k : ℕ, a * k < n ∧ n < a * (k + 1)) :=
  not_dvd_iff_lt_mul_succ n ha

Characterization of non-divisibility via consecutive multiples

Informal description

For any natural numbers $n$ and $a$ with $a > 0$, the following are equivalent: 1. $a$ does not divide $n$. 2. There exists a natural number $k$ such that $a \cdot k < n < a \cdot (k + 1)$. In other words, $\neg(a \mid n) \leftrightarrow \exists k \in \mathbb{N}, a k < n < a (k + 1)$.

Nat.dvd_right_iff_eq theorem

: (∀ a : ℕ, m ∣ a ↔ n ∣ a) ↔ m = n

Full source

/-- Two natural numbers are equal if and only if they have the same multiples. -/
lemma dvd_right_iff_eq : (∀ a : ℕ, m ∣ a ↔ n ∣ a) ↔ m = n :=
  ⟨fun h => Nat.dvd_antisymm ((h _).mpr (Nat.dvd_refl _)) ((h _).mp (Nat.dvd_refl _)),
    fun h n => by rw [h]⟩

Equality of Natural Numbers via Divisibility of Multiples

Informal description

Two natural numbers $m$ and $n$ are equal if and only if, for every natural number $a$, $m$ divides $a$ if and only if $n$ divides $a$. In other words, $m = n \leftrightarrow (\forall a \in \mathbb{N}, m \mid a \leftrightarrow n \mid a)$.

Nat.dvd_left_iff_eq theorem

: (∀ a : ℕ, a ∣ m ↔ a ∣ n) ↔ m = n

Full source

/-- Two natural numbers are equal if and only if they have the same divisors. -/
lemma dvd_left_iff_eq : (∀ a : ℕ, a ∣ m ↔ a ∣ n) ↔ m = n :=
  ⟨fun h => Nat.dvd_antisymm ((h _).mp (Nat.dvd_refl _)) ((h _).mpr (Nat.dvd_refl _)),
    fun h n => by rw [h]⟩

Natural Numbers are Equal if and only if They Have the Same Divisors

Informal description

For any two natural numbers $m$ and $n$, the following are equivalent: 1. For every natural number $a$, $a$ divides $m$ if and only if $a$ divides $n$. 2. $m = n$. In other words, two natural numbers are equal if and only if they have exactly the same divisors.

Nat.div_lt_div_of_lt_of_dvd theorem

{a b d : ℕ} (hdb : d ∣ b) (h : a < b) : a / d < b / d

Full source

lemma div_lt_div_of_lt_of_dvd {a b d : ℕ} (hdb : d ∣ b) (h : a < b) : a / d < b / d := by
  rw [Nat.lt_div_iff_mul_lt' hdb]
  exact Nat.lt_of_le_of_lt (mul_div_le a d) h

Division Preserves Strict Inequality under Divisibility: $a < b \Rightarrow a/d < b/d$ when $d \mid b$

Informal description

For any natural numbers $a$, $b$, and $d$ such that $d$ divides $b$ and $a < b$, we have $a/d < b/d$.

Nat.decidableLoHi instance

(lo hi : ℕ) (P : ℕ → Prop) [DecidablePred P] : Decidable (∀ x, lo ≤ x → x < hi → P x)

Full source

instance decidableLoHi (lo hi : ℕ) (P : ℕ → Prop) [DecidablePred P] :
    Decidable (∀ x, lo ≤ x → x < hi → P x) :=
  decidable_of_iff (∀ x < hi - lo, P (lo + x)) <| by
    refine ⟨fun al x hl hh ↦ ?_,
      fun al x h ↦ al _ (Nat.le_add_right _ _) (Nat.lt_sub_iff_add_lt'.1 h)⟩
    have := al (x - lo) ((Nat.sub_lt_sub_iff_right hl).2 hh)
    rwa [Nat.add_sub_cancel' hl] at this

Decidability of Bounded Universal Quantification with Strict Upper Bound

Informal description

For any natural numbers `lo` and `hi`, and any predicate `P` on natural numbers with a decidable truth value, the statement `∀ x, lo ≤ x → x < hi → P x` is decidable.

Nat.decidableLoHiLe instance

(lo hi : ℕ) (P : ℕ → Prop) [DecidablePred P] : Decidable (∀ x, lo ≤ x → x ≤ hi → P x)

Full source

instance decidableLoHiLe (lo hi : ℕ) (P : ℕ → Prop) [DecidablePred P] :
    Decidable (∀ x, lo ≤ x → x ≤ hi → P x) :=
  decidable_of_iff (∀ x, lo ≤ x → x < hi + 1 → P x) <|
    forall₂_congr fun _ _ ↦ imp_congr Nat.lt_succ_iff Iff.rfl

Decidability of Bounded Universal Quantification on Natural Numbers

Informal description

For any natural numbers `lo` and `hi`, and any predicate `P` on natural numbers with decidable truth values, the statement "for all `x` such that `lo ≤ x ≤ hi`, `P x` holds" is decidable.