no goals
𝕜 : Type u_1
𝕜' : Type ?u.241289
E : Type u_2
E' : Type ?u.241295
F : Type ?u.241298
ι : Type ?u.241301
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ r < r + 1
linarith