lean_workbook_plus_66158

Proved

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

Prove that for every $0<x,y<1$ :\nx\ge y\implies x^n \ge y^n

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66158 (n : ℕ) (x y : ℝ) (hx : 0 < x ∧ x < 1) (hy : 0 < y ∧ y < 1) (hxy : x ≥ y) : x^n ≥ y^n   :=  by sorry

Source