[STATEMENT]
lemma directional_derivative_add[simp]: "directional_derivative k a (x + y) = directional_derivative k a x + directional_derivative k a y"
  and directional_derivative_scaleR[simp]: "directional_derivative k a (c *\<^sub>R x) = c *\<^sub>R directional_derivative k a x"
  if "k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. directional_derivative k a (x + y) = directional_derivative k a x + directional_derivative k a y &&& directional_derivative k a (c *\<^sub>R x) = c *\<^sub>R directional_derivative k a x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0

goal (1 subgoal):
 1. directional_derivative k a (x + y) = directional_derivative k a x + directional_derivative k a y &&& directional_derivative k a (c *\<^sub>R x) = c *\<^sub>R directional_derivative k a x
[PROOF STEP]
by (auto simp: directional_derivative_def restrict0_def[abs_def] fun_eq_iff
      differentiable_on_def linear_iff that
      dest!: linear_frechet_derivative spec[where x=a] smooth_on_imp_differentiable_on)