lean_workbook_plus_6707
ProvedThe 2nd, if , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6707 (a b : ℝ) (h₀ : 0 ≤ a ∧ 0 ≤ b) (h₁ : a ≤ b) : a / (1 + a) ≤ b / (1 + b) := by sorry
Source
The 2nd, if , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_6707 (a b : ℝ) (h₀ : 0 ≤ a ∧ 0 ≤ b) (h₁ : a ≤ b) : a / (1 + a) ≤ b / (1 + b) := by sorry