the first order condition for quasiconvex function

theorem Quasiconvex_first_order_condition_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {f' : E → E →L[ℝ] ℝ} {s : Set E} {x : E} (h : HasFDerivAt f (f' x) x) (xs : x ∈ s) (hf : QuasiconvexOn ℝ s f) (y : E) : y ∈ s → f y ≤ f x → (f' x) (y - x) ≤ 0