𝕜 : Type ?u.62097
E : Type u_1
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ¬SameRay ℝ (x - y + y) y
⊢ ‖x - y + y‖ - ‖y‖ < ‖x - y‖
𝕜 : Type ?u.62097
E : Type u_1
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ¬SameRay ℝ x y
⊢ ‖x‖ - ‖y‖ < ‖x - y‖
nth_rw 1 [← sub_add_cancel x y] at h⊢
no goals
𝕜 : Type ?u.62097
E : Type u_1
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ¬SameRay ℝ (x - y + y) y
⊢ ‖x - y + y‖ - ‖y‖ < ‖x - y‖
exact sub_lt_iff_lt_add.2 (norm_add_lt_of_not_sameRay fun H' => h <| H'.add_left SameRay.rfl)