∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a y : E},
  IsLocalMinOn f s a → y ∈ posTangentConeAt s a → -y ∈ posTangentConeAt s a → (fderivWithin ℝ f s a) y = 0