[STATEMENT]
lemma has_vector_derivative_divide[derivative_intros]:
  fixes a :: "'a::real_normed_field"
  shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x / a) has_vector_derivative (x / a)) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x / a) has_vector_derivative x / a) F
[PROOF STEP]
unfolding divide_inverse
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x * inverse a) has_vector_derivative x * inverse a) F
[PROOF STEP]
by (fact has_vector_derivative_mult_left)