linear_combination with an inverse atom: add the x*x⁻¹=1 fact as an extra term

When the hypothesis contains (r^a)⁻¹ and the goal does not (e.g. solving P·(r^b−1) + (1−P)·((r^a)⁻¹−1) = 0 for P), field_simp at h then linear_combination c * h may fail because field_simp rearranges unpredictably. More robust: keep h as is, prove key : r^a * (r^a)⁻¹ = 1 := mul_inv_cancel₀ hu.ne', and write linear_combination (-(r^a)) * h + (1 - P) * key; ring treats (r^a)⁻¹ as an atom and key supplies the cancellation. Also: zpow_lt_one₀ takes 0 < a (not 0 ≤ a), and zpow_le_zpow_right₀ / zpow_le_zpow_right_of_le_one₀ give the monotone bound r^z ≤ r^m + r^n for z ∈ [m,n] with a case split on 1 ≤ r.