lean_workbook_plus_3255

Proved

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

Explain why $ \frac{1+x^{30}}{1+x^{60}} < 1 + x^{30} $ for $ 0<x\leq 1 $

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3255 (x : ℝ) (hx : 0 < x ∧ x ≤ 1) :
  (1 + x^30) / (1 + x^60) < 1 + x^30   :=  by sorry

Source