Prove2Me

lean_workbook_plus_18678

Proved

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

Given a,b,m,na, b, m, n natural numbers a<b ,  m<na < b \ , \ \ m < n satisfied: a−b=m−n     a+b≥m+na-b = m - n \ \ \ \ \ a + b \ge m + n Prove (or disproof) that ab≥mn\frac{a}{b} \ge \frac{m}{n}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_18678 (a b m n : ℕ) (h₁ : a < b ∧ m < n) (h₂ : a - b = m - n) (h₃ : a + b ≥ m + n) : a / b ≥ m / n   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph