a✝ b✝ : ℤ
n✝ : ℕ
this : ∀ (a : ℤ) (n : ℕ), abs (a / ↑n) ≤ abs a
a b : ℤ
n : ℕ
⊢ abs (a / ↑n) ≤ abs a
a✝ b✝ : ℤ
n✝ : ℕ
this : ∀ (a : ℤ) (n : ℕ), abs (a / ↑n) ≤ abs a
a b : ℤ
n : ℕ
⊢ abs (a / -↑n) ≤ abs a
rw [Int.ediv_neg, abs_neg]
no goals
a✝ b✝ : ℤ
n✝ : ℕ
this : ∀ (a : ℤ) (n : ℕ), abs (a / ↑n) ≤ abs a
a b : ℤ
n : ℕ
⊢ abs (a / ↑n) ≤ abs a
apply this
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ ↑(natAbs (a / ↑n)) ≤ ↑(natAbs a)
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ abs (a / ↑n) ≤ abs a
rw [abs_eq_natAbs, abs_eq_natAbs]
no goals
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ ↑(natAbs (a / ↑n)) ≤ ↑(natAbs a)
exact
  ofNat_le_ofNat_of_le
    (match a, n with
    | (m : ℕ), n => Nat.div_le_self _ _
    | -[m+1], 0 => Nat.zero_le _
    | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))