rw [← one_add_div h_k_nonzero, h₁, add_le_add_iff_left,
  one_div_le_one_div h_p_pred_pos hk, @le_sub_iff_add_le]
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
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)
⊢ k + 1 ≤ p