theorem perCapitaSurplus_le_peak {J ρ : ℝ} (hJ : 1 < J) (hρ : ρ < 1) :
    perCapitaSurplus J ρ ≤ (1 - ρ) / 4 := by
  rw [← perCapitaSurplus_at_two ρ]
  by_cases h2 : J ≤ 2
  · rcases (lt_or_eq_of_le h2) with hlt | heq
    · exact le_of_lt (perCapitaSurplus_increasing_below_peak hJ hlt le_rfl hρ)
    · rw [heq]
  · push_neg at h2
    exact le_of_lt (perCapitaSurplus_decreasing_above_peak le_rfl h2 hρ)

theorem curvatureKReal_increasing {ρ : ℝ} (hρ : ρ < 1) :
    ∀ J₁ J₂ : ℝ, 0 < J₁ → J₁ < J₂ →
    curvatureKReal J₁ ρ < curvatureKReal J₂ ρ := by
  intro J₁ J₂ hJ₁ hJ₁₂
  simp only [curvatureKReal]
  have h1ρ : 0 < 1 - ρ := by linarith
  have hJ₂ : 0 < J₂ := by linarith
  -- (1-ρ)(J₁-1)/J₁ < (1-ρ)(J₂-1)/J₂
  -- ⟺ (J₁-1)/J₁ < (J₂-1)/J₂  (since 1-ρ > 0)
  -- ⟺ (J₁-1)J₂ < (J₂-1)J₁    (cross multiply)
  -- ⟺ J₁J₂ - J₂ < J₁J₂ - J₁
  -- ⟺ J₁ < J₂  ✓
  rw [div_lt_div_iff₀ hJ₁ hJ₂]
  nlinarith

theorem curvatureK_real_increasing {ρ : ℝ} (hρ : ρ < 1) :
    ∀ J₁ J₂ : ℝ, 0 < J₁ → J₁ < J₂ →
    curvatureK_real J₁ ρ < curvatureK_real J₂ ρ := by
  intro J₁ J₂ hJ₁ hJ₁₂
  simp only [curvatureK_real]
  have h1ρ : 0 < 1 - ρ := by linarith
  have hJ₂ : 0 < J₂ := by linarith
  -- (1-ρ)(J₁-1)/J₁ < (1-ρ)(J₂-1)/J₂
  -- ⟺ (J₁-1)/J₁ < (J₂-1)/J₂  (since 1-ρ > 0)
  -- ⟺ (J₁-1)J₂ < (J₂-1)J₁    (cross multiply)
  -- ⟺ J₁J₂ - J₂ < J₁J₂ - J₁
  -- ⟺ J₁ < J₂  ✓
  rw [div_lt_div_iff₀ hJ₁ hJ₂]
  nlinarith