add_inv_mono_on_one

proof body

Tactic-mode proof.

  75  have hxpos : 0 < x := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hx1
  76  have hypos : 0 < y := lt_of_lt_of_le hxpos hxy
  77  have hxy1 : 1 ≤ x * y := by
  78    nlinarith [hx1, hxy]
  79  have hfac : (y + y⁻¹) - (x + x⁻¹) = (y - x) * (1 - (x * y)⁻¹) := by
  80    field_simp [hxpos.ne', hypos.ne']
  81    ring
  82  have hA : 0 ≤ y - x := sub_nonneg.mpr hxy
  83  have hB : 0 ≤ 1 - (x * y)⁻¹ := by
  84    have hrepr : 1 - (x * y)⁻¹ = ((x * y) - 1) / (x * y) := by
  85      field_simp [hxpos.ne', hypos.ne']
  86    rw [hrepr]
  87    exact div_nonneg (sub_nonneg.mpr hxy1) (le_of_lt (mul_pos hxpos hypos))
  88  have hdiff : 0 ≤ (y + y⁻¹) - (x + x⁻¹) := by
  89    rw [hfac]
  90    exact mul_nonneg hA hB
  91  linarith
  92
  93/-- On `[1,∞)`, `Jcost` is monotone increasing. -/