lean_workbook_plus_63128
ProvedProve this: \n[mx] + [nx] <= [(m+n)*x]\nDo you mean: $\lfloor m\cdot x\rfloor+\lfloor n\cdot x\rfloor\le\lfloor(m+n)\cdot x\rfloor$ where that's the greatest integer function?
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_63128 (m n x : ℝ) : (Int.floor (m * x) + Int.floor (n * x) : ℝ) ≤ Int.floor ((m + n) * x) := by sorry
Source