-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c = a / c + b :=
  suffices ∀ {{a b c : Int}}, 0 < c → (a + b * c).ediv c = a.ediv c + b from
    match Int.lt_trichotomy c 0 with
    | Or.inl hlt => by
      rw [← Int.neg_inj, ← Int.ediv_neg, Int.neg_add, ← Int.ediv_neg, ← Int.neg_mul_neg]
      exact this (Int.neg_pos_of_neg hlt)
    | Or.inr (Or.inl HEq) => absurd HEq H
    | Or.inr (Or.inr hgt) => this hgt
  suffices ∀ {k n : Nat} {a : Int}, (a + n * k.succ).ediv k.succ = a.ediv k.succ + n from
    fun a b c H => match c, eq_succ_of_zero_lt H, b with
      | _, ⟨_, rfl⟩, ofNat _ => this
      | _, ⟨k, rfl⟩, -[n+1] => show (a - n.succ * k.succ).ediv k.succ = a.ediv k.succ - n.succ by
        rw [← Int.add_sub_cancel (ediv ..), ← this, Int.sub_add_cancel]
  fun {k n} => @fun
  | ofNat _ => congrArg ofNat <| Nat.add_mul_div_right _ _ k.succ_pos
  | -[m+1] => by
    show ((n * k.succ : Nat) - m.succ : Int).ediv k.succ = n - (m / k.succ + 1 : Nat)
    by_cases h : m < n * k.succ
    · rw [← Int.ofNat_sub h, ← Int.ofNat_sub ((Nat.div_lt_iff_lt_mul k.succ_pos).2 h)]
      apply congrArg ofNat
      rw [Nat.mul_comm, Nat.mul_sub_div]; rwa [Nat.mul_comm]
    · have h := Nat.not_lt.1 h
      have H {a b : Nat} (h : a ≤ b) : (a : Int) + -((b : Int) + 1) = -[b - a +1]

Proof state:
a b c : Int
H : c ≠ 0
this : ∀ ⦃a b c : Int⦄, 0 < c → (a + b * c).ediv c = a.ediv c + b
hlt : c < 0
⊢ (a + -b * -c) / -c = a / -c + -b

Tactic:
exact this (Int.neg_pos_of_neg hlt)

Result:
no goals

Proof state:
a b c : Int
H : c ≠ 0
k n m : Nat
⊢ (↑(n * k.succ) - ↑m.succ).ediv ↑k.succ = ↑n - ↑(m / k.succ + 1)

Tactic:
by_cases h : m < n * k.succ

Result:
case pos
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * k.succ
⊢ (↑(n * k.succ) - ↑m.succ).ediv ↑k.succ = ↑n - ↑(m / k.succ + 1)

case neg
a b c : Int
H : c ≠ 0
k n m : Nat
h : ¬m < n * k.succ
⊢ (↑(n * k.succ) - ↑m.succ).ediv ↑k.succ = ↑n - ↑(m / k.succ + 1)

Proof state:
a✝ b✝ c✝ : Int
H✝ : c✝ ≠ 0
this : ∀ {k n : Nat} {a : Int}, (a + ↑n * ↑k.succ).ediv ↑k.succ = a.ediv ↑k.succ + ↑n
a b c : Int
k n : Nat
H : 0 < ↑k.succ
⊢ (a - ↑n.succ * ↑k.succ).ediv ↑k.succ = a.ediv ↑k.succ - ↑n.succ

Tactic:
rw [← Int.add_sub_cancel (ediv ..), ← this, Int.sub_add_cancel]

Result:
no goals

Proof state:
case pos
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * k.succ
⊢ (n * k.succ - m.succ) / k.succ = n - (m / k.succ).succ

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

Result:
case pos.h₁
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * k.succ
⊢ m < k.succ * n

Proof state:
a✝ b✝ c : Int
H : c ≠ 0
k n m : Nat
h✝¹ : ¬m < n * k.succ
h✝ : n * k.succ ≤ m
a b : Nat
h : a ≤ b
⊢ ↑a + -(↑b + 1) = -[b - a+1]

Tactic:
rw [negSucc_eq, Int.ofNat_sub h]

Result:
a✝ b✝ c : Int
H : c ≠ 0
k n m : Nat
h✝¹ : ¬m < n * k.succ
h✝ : n * k.succ ≤ m
a b : Nat
h : a ≤ b
⊢ ↑a + -(↑b + 1) = -(↑b - ↑a + 1)

Proof state:
case neg
a b c : Int
H : c ≠ 0
k n m : Nat
h : ¬m < n * k.succ
⊢ (↑(n * k.succ) - ↑m.succ).ediv ↑k.succ = ↑n - ↑(m / k.succ + 1)

Tactic:
have h := Nat.not_lt.1 h

Result:
case neg
a b c : Int
H : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
⊢ (↑(n * k.succ) - ↑m.succ).ediv ↑k.succ = ↑n - ↑(m / k.succ + 1)

Proof state:
case pos
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * k.succ
⊢ (↑(n * k.succ - m.succ)).ediv ↑k.succ = ↑(n - (m / k.succ).succ)

Tactic:
apply congrArg ofNat

Result:
case pos
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * k.succ
⊢ (n * k.succ - m.succ) / k.succ = n - (m / k.succ).succ

Proof state:
case neg
a b c : Int
H : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
⊢ (↑(n * k.succ) - ↑m.succ).ediv ↑k.succ = ↑n - ↑(m / k.succ + 1)

Tactic:
have H {a b : Nat} (h : a ≤ b) : (a : Int) + -((b : Int) + 1) = -[b - a +1] := by
  rw [negSucc_eq, Int.ofNat_sub h]
  simp only [Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, Int.add_left_comm, Int.add_assoc]

Result:
case neg
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ (↑(n * k.succ) - ↑m.succ).ediv ↑k.succ = ↑n - ↑(m / k.succ + 1)

Proof state:
case pos
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * k.succ
⊢ (↑(n * k.succ) - ↑m.succ).ediv ↑k.succ = ↑n - ↑(m / k.succ + 1)

Tactic:
rw [← Int.ofNat_sub h, ← Int.ofNat_sub ((Nat.div_lt_iff_lt_mul k.succ_pos).2 h)]

Result:
case pos
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * k.succ
⊢ (↑(n * k.succ - m.succ)).ediv ↑k.succ = ↑(n - (m / k.succ).succ)

Proof state:
case neg
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ (↑(n * k.succ) + -(↑m + 1)).ediv ↑k.succ = ↑n + -(↑(m / k.succ) + 1)

Tactic:
rw [H h, H ((Nat.le_div_iff_mul_le k.succ_pos).2 h)]

Result:
case neg
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ -[m - n * k.succ+1].ediv ↑k.succ = -[m / k.succ - n+1]

Proof state:
a b c : Int
H : c ≠ 0
this : ∀ ⦃a b c : Int⦄, 0 < c → (a + b * c).ediv c = a.ediv c + b
hlt : c < 0
⊢ (a + b * c) / c = a / c + b

Tactic:
rw [← Int.neg_inj, ← Int.ediv_neg, Int.neg_add, ← Int.ediv_neg, ← Int.neg_mul_neg]

Result:
a b c : Int
H : c ≠ 0
this : ∀ ⦃a b c : Int⦄, 0 < c → (a + b * c).ediv c = a.ediv c + b
hlt : c < 0
⊢ (a + -b * -c) / -c = a / -c + -b

Proof state:
a b c : Int
H : c ≠ 0
k n m : Nat
⊢ (-[m+1] + ↑n * ↑k.succ).ediv ↑k.succ = -[m+1].ediv ↑k.succ + ↑n

Tactic:
show ((n * k.succ : Nat) - m.succ : Int).ediv k.succ = n - (m / k.succ + 1 : Nat)

Result:
a b c : Int
H : c ≠ 0
k n m : Nat
⊢ (↑(n * k.succ) - ↑m.succ).ediv ↑k.succ = ↑n - ↑(m / k.succ + 1)

Proof state:
case neg.h₁
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ k.succ * n ≤ m

Tactic:
rwa [Nat.mul_comm]

Result:
no goals

Proof state:
case neg
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ -[m - n * k.succ+1].ediv ↑k.succ = -[m / k.succ - n+1]

Tactic:
apply congrArg negSucc

Result:
case neg
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ (m - n * k.succ) / k.succ = m / k.succ - n

Proof state:
case neg
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ (m - n * k.succ) / k.succ = m / k.succ - n

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

Result:
case neg.h₁
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ k.succ * n ≤ m

Proof state:
a✝ b✝ c : Int
H : c ≠ 0
k n m : Nat
h✝¹ : ¬m < n * k.succ
h✝ : n * k.succ ≤ m
a b : Nat
h : a ≤ b
⊢ ↑a + -(↑b + 1) = -(↑b - ↑a + 1)

Tactic:
simp only [Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, Int.add_left_comm, Int.add_assoc]

Result:
no goals

Proof state:
case pos.h₁
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * k.succ
⊢ m < k.succ * n

Tactic:
rwa [Nat.mul_comm]

Result:
no goals

Proof state:
case neg
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ (↑(n * k.succ) - ↑m.succ).ediv ↑k.succ = ↑n - ↑(m / k.succ + 1)

Tactic:
show ediv (↑(n * succ k) + -((m : Int) + 1)) (succ k) = n + -(↑(m / succ k) + 1 : Int)

Result:
case neg
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * k.succ
h : n * k.succ ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ (↑(n * k.succ) + -(↑m + 1)).ediv ↑k.succ = ↑n + -(↑(m / k.succ) + 1)