a b c : Int
this : ∀ (m k : Nat) (b : Int), ↑(succ m) * b / (↑(succ m) * ↑k) = b / ↑k
m k : Nat
H : 0 < ↑(succ m)
⊢ -(↑(succ m) * b / (↑(succ m) * ↑k)) = -(b / ↑k)
a b c : Int
this : ∀ (m k : Nat) (b : Int), ↑(succ m) * b / (↑(succ m) * ↑k) = b / ↑k
m k : Nat
H : 0 < ↑(succ m)
⊢ ↑(succ m) * b / (↑(succ m) * -↑k) = b / -↑k
rw [Int.mul_neg, Int.ediv_neg, Int.ediv_neg]
a b c : Int
this : ∀ (m k : Nat) (b : Int), ↑(succ m) * b / (↑(succ m) * ↑k) = b / ↑k
m k : Nat
H : 0 < ↑(succ m)
⊢ ↑(succ m) * b / (↑(succ m) * ↑k) = b / ↑k
a b c : Int
this : ∀ (m k : Nat) (b : Int), ↑(succ m) * b / (↑(succ m) * ↑k) = b / ↑k
m k : Nat
H : 0 < ↑(succ m)
⊢ -(↑(succ m) * b / (↑(succ m) * ↑k)) = -(b / ↑k)
apply congrArg Neg.neg
no goals
a b c : Int
this : ∀ (m k : Nat) (b : Int), ↑(succ m) * b / (↑(succ m) * ↑k) = b / ↑k
m k : Nat
H : 0 < ↑(succ m)
⊢ ↑(succ m) * b / (↑(succ m) * ↑k) = b / ↑k
apply this
no goals
a b✝ c : Int
H : 0 < a
m k : Nat
b : Int
n : Nat
⊢ ↑(succ m) * -[n+1] / (↑(succ m) * ↑0) = -[n+1] / ↑0
rw [Int.ofNat_zero, Int.mul_zero, Int.ediv_zero, Int.ediv_zero]
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / succ k * (succ m * succ k) ≤ succ m * n + m

case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ succ m * n + m < succ (n / succ k) * (succ m * succ k)
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ (succ m * n + m) / (succ m * succ k) = n / succ k
apply Nat.div_eq_of_lt_le
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / succ k * (succ m * succ k) ≤ succ m * n
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / succ k * (succ m * succ k) ≤ succ m * n + m
refine Nat.le_trans ?_ (Nat.le_add_right _ _)
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ succ m * n / (succ m * succ k) * (succ m * succ k) ≤ succ m * n
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / succ k * (succ m * succ k) ≤ succ m * n
rw [← Nat.mul_div_mul_left _ _ m.succ_pos]
no goals
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ succ m * n / (succ m * succ k) * (succ m * succ k) ≤ succ m * n
apply Nat.div_mul_le_self
case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ succ m * succ n ≤ succ (n / succ k) * (succ m * succ k)
case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ succ m * n + m < succ (n / succ k) * (succ m * succ k)
show m.succ * n.succ ≤ _
case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ succ m * succ n ≤ succ m * (succ (n / succ k) * succ k)
case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ succ m * succ n ≤ succ (n / succ k) * (succ m * succ k)
rw [Nat.mul_left_comm]
case hi.h
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ succ n ≤ succ (n / succ k) * succ k
case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ succ m * succ n ≤ succ m * (succ (n / succ k) * succ k)
apply Nat.mul_le_mul_left
case hi.h
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / succ k < succ (n / succ k)
case hi.h
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ succ n ≤ succ (n / succ k) * succ k
apply (Nat.div_lt_iff_lt_mul k.succ_pos).1
no goals
case hi.h
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / succ k < succ (n / succ k)
apply Nat.lt_succ_self