Mediant_is_Between
Provedproofwikireal-analysis
If a/b < c/d with b,d > 0, then a/b < (a+c)/(b+d) < c/d.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Mediant_is_Between (a b c d : ℝ) (hb : 0 < b) (hd : 0 < d) (h : a / b < c / d) : a / b < (a + c) / (b + d) ∧ (a + c) / (b + d) < c / d := by sorry
Source