Init.Data.Nat.Div.Lemmas

Nat.mod_add_mod_lt theorem

(a b : Nat) {c : Nat} (h : 0 < c) : a % c + b % c < 2 * c - 1

Full source

theorem mod_add_mod_lt (a b : Nat) {c : Nat} (h : 0 < c) : a % c + b % c < 2 * c - 1 := by
  have := mod_lt a h
  have := mod_lt b h
  omega

Upper Bound on Sum of Remainders: $a \bmod c + b \bmod c < 2c - 1$

Informal description

For any natural numbers $a$, $b$, and $c$ with $c > 0$, the sum of the remainders $a \bmod c$ and $b \bmod c$ is strictly less than $2c - 1$.

Nat.mod_add_mod_eq theorem

{a b c : Nat} : a % c + b % c = (a + b) % c + if a % c + b % c < c then 0 else c

Full source

theorem mod_add_mod_eq {a b c : Nat} : a % c + b % c = (a + b) % c + if a % c + b % c < c then 0 else c := by
  if h : 0 < c then
    rw [add_mod]
    split <;> rename_i h'
    · simp [mod_eq_of_lt h']
    · have : (a % c + b % c) % c = a % c + b % c - c := by
        rw [mod_eq_iff]
        right
        have := mod_lt a h
        have := mod_lt b h
        exact ⟨by omega, ⟨1, by simp; omega⟩⟩
      omega
  else
    replace h : c = 0 := by omega
    simp [h]

Sum of Remainders Equals Remainder of Sum Plus Adjustment

Informal description

For any natural numbers $a$, $b$, and $c$, the sum of the remainders $a \bmod c$ and $b \bmod c$ equals the remainder of their sum $(a + b) \bmod c$ plus an adjustment term: if $a \bmod c + b \bmod c < c$, the adjustment is $0$, otherwise it is $c$. In other words: $$a \bmod c + b \bmod c = (a + b) \bmod c + \begin{cases} 0 & \text{if } a \bmod c + b \bmod c < c \\ c & \text{otherwise} \end{cases}$$

Nat.add_mod_eq_sub theorem

: (a + b) % c = a % c + b % c - if a % c + b % c < c then 0 else c

Full source

theorem add_mod_eq_sub : (a + b) % c = a % c + b % c - if a % c + b % c < c then 0 else c := by
  conv => rhs; congr; rw [mod_add_mod_eq]
  omega

Remainder of Sum Equals Adjusted Sum of Remainders: $(a + b) \bmod c = (a \bmod c + b \bmod c) - \text{adjustment}$

Informal description

For any natural numbers $a$, $b$, and $c$, the remainder of the sum $(a + b) \bmod c$ equals the sum of the remainders $a \bmod c + b \bmod c$ minus an adjustment term: if $a \bmod c + b \bmod c < c$, the adjustment is $0$, otherwise it is $c$. In other words: $$(a + b) \bmod c = (a \bmod c + b \bmod c) - \begin{cases} 0 & \text{if } a \bmod c + b \bmod c < c \\ c & \text{otherwise} \end{cases}$$

Nat.lt_div_iff_mul_lt theorem

(h : 0 < k) : x < y / k ↔ x * k < y - (k - 1)

Full source

theorem lt_div_iff_mul_lt (h : 0 < k) : x < y / k ↔ x * k < y - (k - 1) := by
  have t := le_div_iff_mul_le h (x := x + 1) (y := y)
  rw [succ_le, add_one_mul] at t
  have s : k = k - 1 + 1 := by omega
  conv at t => rhs; lhs; rhs; rw [s]
  rw [← Nat.add_assoc, succ_le, add_lt_iff_lt_sub_right] at t
  exact t

Inequality Relating Division and Multiplication in Natural Numbers: $x < \lfloor y / k \rfloor \leftrightarrow x \cdot k < y - (k - 1)$

Informal description

For any natural numbers $x$, $y$, and $k$ with $k > 0$, the inequality $x < \lfloor y / k \rfloor$ holds if and only if $x \cdot k < y - (k - 1)$.

Nat.div_le_iff_le_mul theorem

(h : 0 < k) : x / k ≤ y ↔ x ≤ y * k + k - 1

Full source

theorem div_le_iff_le_mul (h : 0 < k) : x / k ≤ y ↔ x ≤ y * k + k - 1 := by
  rw [le_iff_lt_add_one, Nat.div_lt_iff_lt_mul h, Nat.add_one_mul]
  omega

Division-Multiplication Inequality for Natural Numbers: $\frac{x}{k} \leq y \leftrightarrow x \leq yk + k - 1$

Informal description

For any natural numbers $x$, $y$, and $k$ with $k > 0$, the inequality $\frac{x}{k} \leq y$ holds if and only if $x \leq y \cdot k + k - 1$.

Nat.div_eq_iff theorem

(h : 0 < k) : x / k = y ↔ y * k ≤ x ∧ x ≤ y * k + k - 1

Full source

protected theorem div_eq_iff (h : 0 < k) : x / k = y ↔ y * k ≤ x ∧ x ≤ y * k + k - 1 := by
  rw [Nat.eq_iff_le_and_ge, and_comm, le_div_iff_mul_le h, Nat.div_le_iff_le_mul h]

Characterization of Natural Number Division: $\frac{x}{k} = y \leftrightarrow yk \leq x \leq yk + k - 1$

Informal description

For any natural numbers $x$, $y$, and $k$ with $k > 0$, the equality $\frac{x}{k} = y$ holds if and only if $y \cdot k \leq x$ and $x \leq y \cdot k + k - 1$.

Nat.lt_of_div_eq_zero theorem

(h : 0 < k) (h' : x / k = 0) : x < k

Full source

theorem lt_of_div_eq_zero (h : 0 < k) (h' : x / k = 0) : x < k := by
  rw [Nat.div_eq_iff h] at h'
  omega

Zero Division Implies Strict Inequality: $x / k = 0 \Rightarrow x < k$

Informal description

For any natural numbers $x$ and $k$ with $k > 0$, if the integer division of $x$ by $k$ equals zero (i.e., $x / k = 0$), then $x$ is strictly less than $k$ (i.e., $x < k$).

Nat.div_eq_zero_iff_lt theorem

(h : 0 < k) : x / k = 0 ↔ x < k

Full source

theorem div_eq_zero_iff_lt (h : 0 < k) : x / k = 0 ↔ x < k :=
  ⟨lt_of_div_eq_zero h, fun h' => Nat.div_eq_of_lt h'⟩

Zero Division Equivalence: $x / k = 0 \leftrightarrow x < k$

Informal description

For any natural numbers $x$ and $k$ with $k > 0$, the integer division $x / k$ equals zero if and only if $x$ is strictly less than $k$, i.e., $x / k = 0 \leftrightarrow x < k$.

Nat.div_mul_self_eq_mod_sub_self theorem

{x k : Nat} : (x / k) * k = x - (x % k)

Full source

theorem div_mul_self_eq_mod_sub_self {x k : Nat} : (x / k) * k = x - (x % k) := by
  have := mod_eq_sub_div_mul (x := x) (k := k)
  have := div_mul_le_self x k
  omega

Division-Multiplication Identity: $(x / k) * k = x - (x \% k)$

Informal description

For any natural numbers $x$ and $k$, the product of the integer division $x / k$ and $k$ equals $x$ minus the remainder of $x$ divided by $k$, i.e., $(x / k) * k = x - (x \% k)$.

Nat.mul_div_self_eq_mod_sub_self theorem

{x k : Nat} : k * (x / k) = x - (x % k)

Full source

theorem mul_div_self_eq_mod_sub_self {x k : Nat} : k * (x / k) = x - (x % k) := by
  rw [Nat.mul_comm, div_mul_self_eq_mod_sub_self]

Commutative Division-Multiplication Identity: $k \cdot (x / k) = x - (x \% k)$

Informal description

For any natural numbers $x$ and $k$, the product of $k$ and the integer division $x / k$ equals $x$ minus the remainder of $x$ divided by $k$, i.e., $k \cdot (x / k) = x - (x \% k)$.

Nat.lt_div_mul_self theorem

(h : 0 < k) (w : k ≤ x) : x - k < x / k * k

Full source

theorem lt_div_mul_self (h : 0 < k) (w : k ≤ x) : x - k < x / k * k := by
  rw [div_mul_self_eq_mod_sub_self]
  have : x % k < k := mod_lt x h
  omega

Inequality for Division-Multiplication Product: $x - k < (x / k) * k$

Informal description

For any natural numbers $x$ and $k$ such that $0 < k$ and $k \leq x$, the difference $x - k$ is strictly less than the product of the integer division $x / k$ and $k$, i.e., $x - k < (x / k) * k$.

Nat.div_pos theorem

(hba : b ≤ a) (hb : 0 < b) : 0 < a / b

Full source

theorem div_pos (hba : b ≤ a) (hb : 0 < b) : 0 < a / b := by
  cases b
  · contradiction
  · simp [Nat.pos_iff_ne_zero, div_eq_zero_iff_lt, hba]

Positivity of Natural Number Division Under Nonzero Divisor

Informal description

For any natural numbers $a$ and $b$ such that $b \leq a$ and $0 < b$, the division $a / b$ is strictly positive, i.e., $0 < a / b$.

Nat.div_le_div_left theorem

(hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c

Full source

theorem div_le_div_left (hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c :=
  (Nat.le_div_iff_mul_le hc).2 <|
    Nat.le_trans (Nat.mul_le_mul_left _ hcb) (Nat.div_mul_le_self a b)

Monotonicity of Natural Number Division with Respect to Divisor Size

Informal description

For any natural numbers $a$, $b$, and $c$ such that $c \leq b$ and $0 < c$, the division $a / b$ is less than or equal to $a / c$.

Nat.div_add_le_right theorem

{z : Nat} (h : 0 < z) (x y : Nat) : x / (y + z) ≤ x / z

Full source

theorem div_add_le_right {z : Nat} (h : 0 < z) (x y : Nat) :
    x / (y + z) ≤ x / z :=
  div_le_div_left (Nat.le_add_left z y) h

Monotonicity of Division with Respect to Divisor Addition: $x / (y + z) \leq x / z$ for $z > 0$

Informal description

For any natural numbers $x$, $y$, and $z$ with $z > 0$, the division $x / (y + z)$ is less than or equal to $x / z$.

Nat.succ_div_of_dvd theorem

{a b : Nat} (h : b ∣ a + 1) : (a + 1) / b = a / b + 1

Full source

theorem succ_div_of_dvd {a b : Nat} (h : b ∣ a + 1) :
    (a + 1) / b = a / b + 1 := by
  replace h := mod_eq_zero_of_dvd h
  cases b with
  | zero => simp at h
  | succ b =>
    by_cases h' : b ≤ a
    · rw [Nat.div_eq]
      simp only [zero_lt_succ, Nat.add_le_add_iff_right, h', and_self, ↓reduceIte,
        Nat.reduceSubDiff, Nat.add_right_cancel_iff]
      obtain ⟨_|k, h⟩ := Nat.dvd_of_mod_eq_zero h
      · simp at h
      · simp only [Nat.mul_add, Nat.add_mul, Nat.one_mul, Nat.mul_one, ← Nat.add_assoc,
          Nat.add_right_cancel_iff] at h
        subst h
        rw [Nat.add_sub_cancel, ← Nat.add_one_mul, mul_div_right _ (zero_lt_succ _), Nat.add_comm,
          Nat.add_mul_div_left _ _ (zero_lt_succ _), Nat.self_eq_add_left, div_eq_of_lt le.refl]
    · simp only [Nat.not_le] at h'
      replace h' : a + 1 < b + 1 := Nat.add_lt_add_right h' 1
      rw [Nat.mod_eq_of_lt h'] at h
      simp at h

Successor Division under Divisibility: $(a + 1)/b = a/b + 1$ when $b \mid a + 1$

Informal description

For any natural numbers $a$ and $b$, if $b$ divides $a + 1$ (i.e., $b \mid a + 1$), then the division $(a + 1) / b$ equals $a / b + 1$.

Nat.succ_div_of_mod_eq_zero theorem

{a b : Nat} (h : (a + 1) % b = 0) : (a + 1) / b = a / b + 1

Full source

theorem succ_div_of_mod_eq_zero {a b : Nat} (h : (a + 1) % b = 0) :
    (a + 1) / b = a / b + 1 := by
  rw [succ_div_of_dvd (by rwa [dvd_iff_mod_eq_zero])]

Successor Division when Remainder is Zero: $(a + 1)/b = a/b + 1$ if $(a + 1) \bmod b = 0$

Informal description

For any natural numbers $a$ and $b$, if the remainder of $(a + 1)$ divided by $b$ is zero (i.e., $(a + 1) \bmod b = 0$), then $(a + 1) / b = a / b + 1$.

Nat.succ_div_of_not_dvd theorem

{a b : Nat} (h : ¬b ∣ a + 1) : (a + 1) / b = a / b

Full source

theorem succ_div_of_not_dvd {a b : Nat} (h : ¬ b ∣ a + 1) :
    (a + 1) / b = a / b := by
  replace h := mt dvd_of_mod_eq_zero h
  cases b with
  | zero => simp
  | succ b =>
    rw [eq_comm, Nat.div_eq_iff (by simp)]
    constructor
    · rw [Nat.div_mul_self_eq_mod_sub_self]
      omega
    · rw [Nat.div_mul_self_eq_mod_sub_self]
      have : (a + 1) % (b + 1) < b + 1 := Nat.mod_lt _ (by simp)
      omega

Successor Division under Non-Divisibility: $(a + 1)/b = a/b$ when $b \nmid a + 1$

Informal description

For any natural numbers $a$ and $b$, if $b$ does not divide $a + 1$ (i.e., $b \nmid a + 1$), then the division $(a + 1) / b$ equals $a / b$.

Nat.succ_div_of_mod_ne_zero theorem

{a b : Nat} (h : (a + 1) % b ≠ 0) : (a + 1) / b = a / b

Full source

theorem succ_div_of_mod_ne_zero {a b : Nat} (h : (a + 1) % b ≠ 0) :
    (a + 1) / b = a / b := by
  rw [succ_div_of_not_dvd (by rwa [dvd_iff_mod_eq_zero])]

Successor Division under Nonzero Remainder: $(a + 1)/b = a/b$ when $(a + 1) \bmod b \neq 0$

Informal description

For any natural numbers $a$ and $b$, if the remainder of $(a + 1)$ divided by $b$ is not zero (i.e., $(a + 1) \bmod b \neq 0$), then $(a + 1) / b = a / b$.

Nat.succ_div theorem

{a b : Nat} : (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0

Full source

protected theorem succ_div {a b : Nat} : (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0 := by
  split <;> rename_i h
  · simp [succ_div_of_dvd h]
  · simp [succ_div_of_not_dvd h]

Division of Successor by Condition: $\frac{a + 1}{b} = \frac{a}{b} + \mathbb{1}_{b \mid (a + 1)}$

Informal description

For any natural numbers $a$ and $b$, the division of $a + 1$ by $b$ satisfies: \[ \frac{a + 1}{b} = \frac{a}{b} + \begin{cases} 1 & \text{if } b \text{ divides } a + 1 \\ 0 & \text{otherwise} \end{cases} \]

Nat.add_div theorem

{a b c : Nat} (h : 0 < c) : (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0

Full source

protected theorem add_div {a b c : Nat} (h : 0 < c) :
    (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0 := by
  conv => lhs; rw [← Nat.div_add_mod a c]
  rw [Nat.add_assoc, mul_add_div h]
  conv => lhs; rw [← Nat.div_add_mod b c]
  rw [Nat.add_comm (a % c), Nat.add_assoc, mul_add_div h, ← Nat.add_assoc, Nat.add_comm (b % c)]
  congr
  rw [Nat.div_eq_iff h]
  constructor
  · split <;> rename_i h
    · simpa using h
    · simp
  · have := mod_lt a h
    have := mod_lt b h
    split <;> · simp; omega

Division of Sum Formula for Natural Numbers with Remainder Condition

Informal description

For any natural numbers $a$, $b$, and $c$ with $c > 0$, the division of the sum $a + b$ by $c$ satisfies: \[ \frac{a + b}{c} = \frac{a}{c} + \frac{b}{c} + \begin{cases} 1 & \text{if } c \leq (a \bmod c) + (b \bmod c) \\ 0 & \text{otherwise} \end{cases} \]

Nat.mod_add_mod_lt_of_add_mod_eq_sub_one theorem

(w : 0 < c) (h : (a + b) % c = c - 1) : a % c + b % c < c

Full source

/-- If `(a + b) % c = c - 1`, then `a % c + b % c < c`, because `a % c + b % c` can not reach `2*c - 1`. -/
theorem mod_add_mod_lt_of_add_mod_eq_sub_one (w : 0 < c) (h : (a + b) % c = c - 1) : a % c + b % c < c := by
  have := mod_add_mod_lt a b w
  rw [mod_add_mod_eq, h] at this
  split at this
  · assumption
  · omega

Sum of Remainders Bounded When Total Remainder is Maximal: $a \bmod c + b \bmod c < c$ if $(a + b) \bmod c = c - 1$

Informal description

For any natural numbers $a$, $b$, and $c$ with $c > 0$, if $(a + b) \bmod c = c - 1$, then the sum of the remainders satisfies $a \bmod c + b \bmod c < c$.

Nat.add_div_of_dvd_add_add_one theorem

(h : c ∣ a + b + 1) : (a + b) / c = a / c + b / c

Full source

theorem add_div_of_dvd_add_add_one (h : c ∣ a + b + 1) : (a + b) / c = a / c + b / c := by
  have w : c ≠ 0 := by rintro rfl; simp at h
  replace w : 0 < c := by omega
  rw [Nat.add_div w, if_neg, Nat.add_zero]
  have := mod_add_mod_lt_of_add_mod_eq_sub_one w ((mod_eq_sub_iff Nat.zero_lt_one w).mpr h)
  omega

Division of Sum When Divisor Divides Sum Plus One: $(a + b)/c = a/c + b/c$ if $c \mid (a + b + 1)$

Informal description

For any natural numbers $a$, $b$, and $c$, if $c$ divides $a + b + 1$, then the integer division of $a + b$ by $c$ equals the sum of the integer divisions of $a$ by $c$ and $b$ by $c$, i.e., $(a + b) / c = a / c + b / c$.

Nat.div_lt_of_lt theorem

{a b c : Nat} (ha : a < c) : a / b < c

Full source

theorem div_lt_of_lt {a b c : Nat} (ha : a < c) : a / b < c := by
  obtain (rfl|hb) := Nat.eq_zero_or_pos b
  · simp
    omega
  · rw [Nat.div_lt_iff_lt_mul hb, ← Nat.mul_one a]
    apply Nat.mul_lt_mul_of_lt_of_le ha (by omega) (by omega)

Integer Division Bounded by Strict Inequality: $a < c \implies a / b < c$

Informal description

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

Nat.div_mod_eq_div theorem

{a b c : Nat} (ha : a < c) : (a / b) % c = a / b

Full source

theorem div_mod_eq_div {a b c : Nat} (ha : a < c) : (a / b) % c = a / b :=
  Nat.mod_eq_of_lt (Nat.div_lt_of_lt ha)

Modulo of Division Equals Division When Dividend is Small: $(a / b) \mod c = a / b$ for $a < c$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $a < c$, the remainder of the integer division $a / b$ when divided by $c$ equals $a / b$ itself, i.e., $(a / b) \mod c = a / b$.

Nat.div_mod_eq_mod_div_mod theorem

{a b c : Nat} (ha : a < c) (hb : b < c) : (a / b) % c = a % c / (b % c)

Full source

theorem div_mod_eq_mod_div_mod {a b c : Nat} (ha : a < c) (hb : b < c) :
    (a / b) % c = a % c / (b % c) := by
  rw [Nat.mod_eq_of_lt (Nat.div_lt_of_lt ha), Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb]

Modulo of Division Equals Division of Moduli under Bounded Conditions

Informal description

For any natural numbers $a$, $b$, and $c$ such that $a < c$ and $b < c$, the remainder of the integer division $a / b$ when divided by $c$ is equal to the integer division of $a \mod c$ by $b \mod c$, i.e., $$(a / b) \mod c = (a \mod c) / (b \mod c).$$

Nat.mod_mod_eq_mod_of_lt_right theorem

{a b c : Nat} (ha : a < c) : (a % b) % c = a % b

Full source

theorem mod_mod_eq_mod_of_lt_right {a b c : Nat} (ha : a < c) : (a % b) % c = a % b :=
  Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt (Nat.mod_le _ _) ha)

Nested Modulo Preservation Under Right Inequality: $(a \mod b) \mod c = a \mod b$ when $a < c$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $a < c$, the remainder of $(a \mod b)$ when divided by $c$ is equal to $a \mod b$.

Nat.mod_mod_eq_mod_mod_mod theorem

{a b c : Nat} (ha : a < c) (hb : b < c) : (a % b) % c = (a % c) % (b % c)

Full source

theorem mod_mod_eq_mod_mod_mod {a b c : Nat} (ha : a < c) (hb : b < c) :
    (a % b) % c = (a % c) % (b % c) := by
  rw [Nat.mod_mod_eq_mod_of_lt_right ha, Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb]

Nested Modulo Equality Under Bounded Conditions: $(a \mod b) \mod c = (a \mod c) \mod (b \mod c)$ when $a, b < c$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $a < c$ and $b < c$, the nested modulo operation satisfies $(a \mod b) \mod c = (a \mod c) \mod (b \mod c)$.

Nat.mod_mod_eq_mod_mod_of_dvd theorem

{a b c : Nat} (h : b ∣ c) : a % b % c = a % c % b

Full source

theorem mod_mod_eq_mod_mod_of_dvd {a b c : Nat} (h : b ∣ c) : a % b % c = a % c % b := by
  refine Or.elim (Nat.eq_zero_or_pos b) (by rintro rfl; simp) (fun hb => ?_)
  refine Or.elim (Nat.eq_zero_or_pos c) (by rintro rfl; simp) (fun hc => ?_)
  rw [Nat.mod_mod_of_dvd _ h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le (Nat.mod_lt a hb) (Nat.le_of_dvd hc h))]

Nested Modulo Commutativity Under Divisibility: $(a \bmod b) \bmod c = (a \bmod c) \bmod b$ when $b \mid c$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $b$ divides $c$, the nested modulo operations satisfy $(a \bmod b) \bmod c = (a \bmod c) \bmod b$.

Nat.mod_mod_of_dvd' theorem

{a b c : Nat} (h : b ∣ c) : a % b % c = a % b

Full source

theorem mod_mod_of_dvd' {a b c : Nat} (h : b ∣ c) : a % b % c = a % b := by
  rw [Nat.mod_mod_eq_mod_mod_of_dvd h, Nat.mod_mod_of_dvd _ h]

Nested Modulo Identity under Divisibility: $(a \bmod b) \bmod c = a \bmod b$ when $b \mid c$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $b$ divides $c$, the nested modulo operation satisfies $(a \bmod b) \bmod c = a \bmod b$.

Nat.mod_mod_eq_mod_mod_mod_of_dvd theorem

{a b c : Nat} (hb : b ∣ c) : (a % b) % c = (a % c) % (b % c)

Full source

theorem mod_mod_eq_mod_mod_mod_of_dvd {a b c : Nat} (hb : b ∣ c) :
    (a % b) % c = (a % c) % (b % c) := by
  refine (Decidable.em (b = c)).elim (by rintro rfl; simp) (fun hb' => ?_)
  refine Or.elim (Nat.eq_zero_or_pos c) (by rintro rfl; simp) (fun hc => ?_)
  have : b < c := Nat.lt_of_le_of_ne (Nat.le_of_dvd hc hb) hb'
  rw [Nat.mod_mod_of_dvd' hb, Nat.mod_eq_of_lt this, Nat.mod_mod_of_dvd _ hb]

Nested Modulo Identity under Divisibility: $(a \bmod b) \bmod c = (a \bmod c) \bmod (b \bmod c)$ when $b \mid c$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $b$ divides $c$, the nested modulo operations satisfy $(a \bmod b) \bmod c = (a \bmod c) \bmod (b \bmod c)$.