have h₁: p / (p - 1) = 1 + 1 / (p - 1) := by
  rw [one_add_div h_p_pred_nonzero, sub_add_cancel]
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
h_p_pred_nonzero : p - 1 ≠ 0
⊢ p / (p - 1) ≤ (k + 1) / k
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
h_p_pred_nonzero : p - 1 ≠ 0
h₁ : p / (p - 1) = 1 + 1 / (p - 1)
⊢ p / (p - 1) ≤ (k + 1) / k