no goals
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ⊤
hy : IsFixedPt f y
⊢ edist x y ≤ edist x (f x) / (1 - ↑K)
simpa only [hy.eq, edist_self, add_zero] using hf.edist_inequality h