abs_ediv_le_abs — Mathlib

English

For all a,b ∈ Z, |a / b| ≤ |a|.

Русский

Пусть a,b ∈ Z. Тогда |a / b| ≤ |a|.

LaTeX

$$$ |a / b| \le |a| $$$

Lean4

theorem abs_ediv_le_abs : ∀ a b : ℤ, |a / b| ≤ |a| :=
  suffices ∀ (a : ℤ) (n : ℕ), |a / n| ≤ |a| from fun a b =>
    match b, Int.eq_nat_or_neg b with
    | _, ⟨n, Or.inl rfl⟩ => this _ _
    | _, ⟨n, Or.inr rfl⟩ => by rw [Int.ediv_neg, abs_neg]; apply this
  fun a n => by rw [abs_eq_natAbs, abs_eq_natAbs];
  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 _ _))

Похожие утверждения