lean_workbook_plus_82407

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwiki

Generalization of Inequality 1: $\left \lfloor \frac{xy}{z} \right \rfloor \ge y \left \lfloor \frac{x}{z} \right \rfloor$ for $x \ge y \ge z; x,y,z \in \mathbb{N}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82407 (x y z : ℕ) (h₁ : x ≥ y) (h₂ : y ≥ z) : (Nat.floor (x * y / z) : ℕ) ≥ y * Nat.floor (x / z)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph