V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ angle x (x + y) < π / 2
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_lt_pi_div_two,
  norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
exact div_pos (norm_pos_iff.2 h0) (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg
  (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)))