lean_workbook_plus_38082

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_38082 (a b : ℝ) (hab : 0 ≤ a ∧ 0 ≤ b ∧ a ≤ b ∧ b ≤ 1) :
  0 ≤ a / (b + 1) + b / (a + 1) ∧ a / (b + 1) + b / (a + 1) ≤ 1   :=  by sorry