lean_workbook_plus_34190

Proved

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

Let the original price be $x$ . We have $(1+\frac{p}{100})(1-\frac{p}{100})x=1$ . Hence, $x=\frac{1}{1-(\frac{p}{100})^2}=\frac {10000}{10000 - p^2}$ , or $\textbf{(E)}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34190  (x p : ℝ)
  (h₀ : 0 < x ∧ 0 < p)
  (h₁ : (1 + p / 100) * (1 - p / 100) * x = 1) :
  x = 10000 / (10000 - p^2)   :=  by sorry

Source

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

View graph