have h_k_nonzero: k ≠ 0 := ne_iff_lt_or_gt.mpr (Or.inr hk)
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
⊢ p / (p - 1) ≤ (k + 1) / k
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
⊢ p / (p - 1) ≤ (k + 1) / k