a b c : Int
H : c ≠ 0
this : ∀ ⦃a b c : Int⦄, 0 < c → ediv (a + b * c) c = ediv a c + b
hlt : c < 0
⊢ (a + -b * -c) / -c = a / -c + -b
a b c : Int
H : c ≠ 0
this : ∀ ⦃a b c : Int⦄, 0 < c → ediv (a + b * c) c = ediv a c + b
hlt : c < 0
⊢ (a + b * c) / c = a / c + b
rw [← Int.neg_inj, ← Int.ediv_neg, Int.neg_add, ← Int.ediv_neg, ← Int.neg_mul_neg]
no goals
a b c : Int
H : c ≠ 0
this : ∀ ⦃a b c : Int⦄, 0 < c → ediv (a + b * c) c = ediv a c + b
hlt : c < 0
⊢ (a + -b * -c) / -c = a / -c + -b
exact this (Int.neg_pos_of_neg hlt)
no goals
a✝ b✝ c✝ : Int
H✝ : c✝ ≠ 0
this : ∀ {k n : Nat} {a : Int}, ediv (a + ↑n * ↑(succ k)) ↑(succ k) = ediv a ↑(succ k) + ↑n
a b c : Int
k n : Nat
H : 0 < ↑(succ k)
⊢ ediv (a - ↑(succ n) * ↑(succ k)) ↑(succ k) = ediv a ↑(succ k) - ↑(succ n)
rw [← Int.add_sub_cancel (ediv ..), ← this, Int.sub_add_cancel]
a b c : Int
H : c ≠ 0
k n m : Nat
⊢ ediv (↑(n * succ k) - ↑(succ m)) ↑(succ k) = ↑n - ↑(m / succ k + 1)
a b c : Int
H : c ≠ 0
k n m : Nat
⊢ ediv (-[m+1] + ↑n * ↑(succ k)) ↑(succ k) = ediv -[m+1] ↑(succ k) + ↑n
show ((n * k.succ : Nat) - m.succ : Int).ediv k.succ = n - (m / k.succ + 1 : Nat)
no goals
a b c : Int
H : c ≠ 0
k n m : Nat
⊢ ediv (↑(n * succ k) - ↑(succ m)) ↑(succ k) = ↑n - ↑(m / succ k + 1)
if h : m < n * k.succ then
  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]
else
  have h := Nat.not_lt.1 h
  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]
  show ediv (↑(n * succ k) + -((m : Int) + 1)) (succ k) = n + -(↑(m / succ k) + 1 : Int)
  rw [H h, H ((Nat.le_div_iff_mul_le k.succ_pos).2 h)]
  apply congrArg negSucc
  rw [Nat.mul_comm, Nat.sub_mul_div]; rwa [Nat.mul_comm]
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * succ k
⊢ ediv ↑(n * succ k - succ m) ↑(succ k) = ↑(n - succ (m / succ k))
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * succ k
⊢ ediv (↑(n * succ k) - ↑(succ m)) ↑(succ k) = ↑n - ↑(m / succ k + 1)
rw [← Int.ofNat_sub h, ← Int.ofNat_sub ((Nat.div_lt_iff_lt_mul k.succ_pos).2 h)]
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * succ k
⊢ (n * succ k - succ m) / succ k = n - succ (m / succ k)
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * succ k
⊢ ediv ↑(n * succ k - succ m) ↑(succ k) = ↑(n - succ (m / succ k))
apply congrArg ofNat
case h₁
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * succ k
⊢ m < succ k * n
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * succ k
⊢ (n * succ k - succ m) / succ k = n - succ (m / succ k)
rw [Nat.mul_comm, Nat.mul_sub_div]
no goals
case h₁
a b c : Int
H : c ≠ 0
k n m : Nat
h : m < n * succ k
⊢ m < succ k * n
rwa [Nat.mul_comm]
a b c : Int
H : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
⊢ ediv (↑(n * succ k) - ↑(succ m)) ↑(succ k) = ↑n - ↑(m / succ k + 1)
a b c : Int
H : c ≠ 0
k n m : Nat
h : ¬m < n * succ k
⊢ ediv (↑(n * succ k) - ↑(succ m)) ↑(succ k) = ↑n - ↑(m / succ k + 1)
have h := Nat.not_lt.1 h
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ ediv (↑(n * succ k) - ↑(succ m)) ↑(succ k) = ↑n - ↑(m / succ k + 1)
a b c : Int
H : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
⊢ ediv (↑(n * succ k) - ↑(succ m)) ↑(succ k) = ↑n - ↑(m / succ k + 1)
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]
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ ediv (↑(n * succ k) + -(↑m + 1)) ↑(succ k) = ↑n + -(↑(m / succ k) + 1)
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ ediv (↑(n * succ k) - ↑(succ m)) ↑(succ k) = ↑n - ↑(m / succ k + 1)
show ediv (↑(n * succ k) + -((m : Int) + 1)) (succ k) = n + -(↑(m / succ k) + 1 : Int)
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ ediv -[m - n * succ k+1] ↑(succ k) = -[m / succ k - n+1]
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ ediv (↑(n * succ k) + -(↑m + 1)) ↑(succ k) = ↑n + -(↑(m / succ k) + 1)
rw [H h, H ((Nat.le_div_iff_mul_le k.succ_pos).2 h)]
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ (m - n * succ k) / succ k = m / succ k - n
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ ediv -[m - n * succ k+1] ↑(succ k) = -[m / succ k - n+1]
apply congrArg negSucc
case h₁
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ succ k * n ≤ m
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ (m - n * succ k) / succ k = m / succ k - n
rw [Nat.mul_comm, Nat.sub_mul_div]
no goals
case h₁
a b c : Int
H✝ : c ≠ 0
k n m : Nat
h✝ : ¬m < n * succ k
h : n * succ k ≤ m
H : ∀ {a b : Nat}, a ≤ b → ↑a + -(↑b + 1) = -[b - a+1]
⊢ succ k * n ≤ m
rwa [Nat.mul_comm]
a✝ b✝ c : Int
H : c ≠ 0
k n m : Nat
h✝¹ : ¬m < n * succ k
h✝ : n * succ k ≤ m
a b : Nat
h : a ≤ b
⊢ ↑a + -(↑b + 1) = -(↑b - ↑a + 1)
a✝ b✝ c : Int
H : c ≠ 0
k n m : Nat
h✝¹ : ¬m < n * succ k
h✝ : n * succ k ≤ m
a b : Nat
h : a ≤ b
⊢ ↑a + -(↑b + 1) = -[b - a+1]
rw [negSucc_eq, Int.ofNat_sub h]
no goals
a✝ b✝ c : Int
H : c ≠ 0
k n m : Nat
h✝¹ : ¬m < n * succ k
h✝ : n * succ k ≤ m
a b : Nat
h : a ≤ b
⊢ ↑a + -(↑b + 1) = -(↑b - ↑a + 1)
simp only [Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, Int.add_left_comm, Int.add_assoc]