-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - (x + 1)) / n = p - ((x / n) + 1)

Proof state:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ x / n < p

Tactic:
rwa [div_lt_iff_lt_mul npos, Nat.mul_comm]

Result:
no goals

Proof state:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ n * p - x ≤ (p - x / n) * n

Tactic:
rw [Nat.mul_sub_right_distrib, Nat.mul_comm]

Result:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ p * n - x ≤ p * n - x / n * n

Proof state:
case lo
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ (p - (x / n + 1)) * n ≤ n * p - (x + 1)

Tactic:
rw [Nat.mul_sub_right_distrib, Nat.mul_comm]

Result:
case lo
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ n * p - (x / n + 1) * n ≤ n * p - (x + 1)

Proof state:
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ (n * p - (x + 1)) / n = p - (x / n + 1)

Tactic:
apply Nat.div_eq_of_lt_le

Result:
case lo
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ (p - (x / n + 1)) * n ≤ n * p - (x + 1)

case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ n * p - (x + 1) < (p - (x / n + 1) + 1) * n

Proof state:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ n * p - (x + 1) < (p - (x / n + 1) + 1) * n

Tactic:
focus
  show succ (pred (n * p - x)) ≤ (succ (pred (p - x / n))) * n
  rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁),
    fun h => succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)] focus
    rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
    exact Nat.sub_le_sub_left (div_mul_le_self ..) _
  focus
    rwa [div_lt_iff_lt_mul npos, Nat.mul_comm]

Result:
no goals

Proof state:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ (n * p - x).pred.succ ≤ (p - x / n).pred.succ * n

Tactic:
rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁),
  fun h => succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)]

Result:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ n * p - x ≤ (p - x / n) * n

case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ x / n < p

Proof state:
x n p : Nat
h₁ : x < 0
n0 : n = 0
⊢ False

Tactic:
exact not_lt_zero _ h₁

Result:
no goals

Proof state:
x n p : Nat
h₁ : x < n * p
⊢ (n * p - (x + 1)) / n = p - (x / n + 1)

Tactic:
have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
  rw [n0, Nat.zero_mul] at h₁; exact not_lt_zero _ h₁

Result:
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ (n * p - (x + 1)) / n = p - (x / n + 1)

Proof state:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ p * n - x ≤ p * n - x / n * n

Tactic:
exact Nat.sub_le_sub_left (div_mul_le_self ..) _

Result:
no goals

Proof state:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ n * p - (x + 1) < (p - (x / n + 1) + 1) * n

Tactic:
show succ (pred (n * p - x)) ≤ (succ (pred (p - x / n))) * n

Result:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ (n * p - x).pred.succ ≤ (p - x / n).pred.succ * n

Proof state:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ n * p - x ≤ (p - x / n) * n

case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ x / n < p

Tactic:
focus
  rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
  exact Nat.sub_le_sub_left (div_mul_le_self ..) _

Result:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ x / n < p

Proof state:
x n p : Nat
h₁ : x < n * p
n0 : n = 0
⊢ False

Tactic:
rw [n0, Nat.zero_mul] at h₁

Result:
x n p : Nat
h₁ : x < 0
n0 : n = 0
⊢ False

Proof state:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ x / n < p

Tactic:
focus
  rwa [div_lt_iff_lt_mul npos, Nat.mul_comm]

Result:
no goals

Proof state:
case lo
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ n * p - (x / n + 1) * n ≤ n * p - (x + 1)

Tactic:
exact Nat.sub_le_sub_left ((div_lt_iff_lt_mul npos).1 (lt_succ_self _)) _

Result:
no goals

Proof state:
case lo
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ (p - (x / n + 1)) * n ≤ n * p - (x + 1)

case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ n * p - (x + 1) < (p - (x / n + 1) + 1) * n

Tactic:
focus
  rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
  exact Nat.sub_le_sub_left ((div_lt_iff_lt_mul npos).1 (lt_succ_self _)) _

Result:
case hi
x n p : Nat
h₁ : x < n * p
npos : 0 < n
⊢ n * p - (x + 1) < (p - (x / n + 1) + 1) * n