case inr
m n k : Nat
kpos : k > 0
⊢ m / n / k = m / (n * k)
m n k : Nat
⊢ m / n / k = m / (n * k)
cases eq_zero_or_pos k with
| inl k0 => rw [k0, Nat.mul_zero, Nat.div_zero, Nat.div_zero] | inr kpos => ?_
case inr.inr
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k = m / (n * k)
case inr
m n k : Nat
kpos : k > 0
⊢ m / n / k = m / (n * k)
cases eq_zero_or_pos n with
| inl n0 => rw [n0, Nat.zero_mul, Nat.div_zero, Nat.zero_div] | inr npos => ?_
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k ≤ m / (n * k)

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k
case inr.inr
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k = m / (n * k)
apply Nat.le_antisymm
no goals
case inl
m n k : Nat
k0 : k = 0
⊢ m / n / k = m / (n * k)
rw [k0, Nat.mul_zero, Nat.div_zero, Nat.div_zero]
no goals
case inr.inl
m n k : Nat
kpos : k > 0
n0 : n = 0
⊢ m / n / k = m / (n * k)
rw [n0, Nat.zero_mul, Nat.div_zero, Nat.zero_div]
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * (n * k) ≤ m
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k ≤ m / (n * k)
apply (le_div_iff_mul_le (Nat.mul_pos npos kpos)).2
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * k * n ≤ m
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * (n * k) ≤ m
rw [Nat.mul_comm n k, ← Nat.mul_assoc]
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * k ≤ m / n
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * k * n ≤ m
apply (le_div_iff_mul_le npos).1
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k ≤ m / n / k
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * k ≤ m / n
apply (le_div_iff_mul_le kpos).1
no goals
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k ≤ m / n / k
(apply Nat.le_refl)
no goals
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k ≤ m / n / k
apply Nat.le_refl
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) * k ≤ m / n
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k
apply (le_div_iff_mul_le kpos).2
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) * k * n ≤ m
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) * k ≤ m / n
apply (le_div_iff_mul_le npos).2
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (k * n) * (k * n) ≤ m
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) * k * n ≤ m
rw [Nat.mul_assoc, Nat.mul_comm n k]
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (k * n) ≤ m / (k * n)
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (k * n) * (k * n) ≤ m
apply (le_div_iff_mul_le (Nat.mul_pos kpos npos)).1
no goals
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (k * n) ≤ m / (k * n)
apply Nat.le_refl