lean_workbook_plus_12280

Proved

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

Let $A(0,0)$ and $B(t,0)$ And point $P(p,0)$ where $0<p<t$ We want to consider $\frac{p}{t-p} <r$ Which is $p <rt-rp$ So $p<\frac{rt}{1+r}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12280 (p t r : ℝ) (h₀ : 0 < p ∧ 0 < t) (h₁ : p < t) (h₂ : 0 < r) : p / (t - p) < r ↔ p < (r * t) / (1 + r)   :=  by sorry

Source