diff --git a/theories/derive.v b/theories/derive.v
index 616ba19ab..fc73e48ee 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -1450,6 +1450,58 @@ rewrite -[ltRHS]invrK ltf_pV2// ?qualifE/= ?invr_gt0 ?subr_gt0 ?imf_ltsup//.
 by rewrite (le_lt_trans (ler_norm _) _) ?imVfltk//; exact: imageP.
 Qed.
 
+Lemma EVT_max_rV (R : realType) n (f : 'rV[R]_n -> R) (A : set 'rV[R]_n) :
+  A !=set0 ->
+  compact A ->
+  {within A, continuous f} -> exists2 c, c \in A &
+  forall t, t \in A -> f t <= f c.
+Proof.
+move=> A0 compactA fcont; set imf := f @` A.
+have imf_sup : has_sup imf.
+  split.
+    case: A0 => a Aa.
+    by exists (f a); apply/imageP.
+  have [M [Mreal imfltM]] : bounded_set (f @` A).
+    exact/compact_bounded/continuous_compact.
+  exists (M + 1) => y /imfltM yleM.
+  by rewrite (le_trans _ (yleM _ _)) ?ler_norm ?ltrDl.
+have [|imf_ltsup] := pselect (exists2 c, c \in A & f c = sup imf).
+  move=> [c cab fceqsup]; exists c => // t tab; rewrite fceqsup.
+  apply/sup_upper_bound => //.
+  exact/imageP/set_mem.
+have {}imf_ltsup t : t \in A -> f t < sup imf.
+  move=> tab; case: (ltrP (f t) (sup imf)) => // supleft.
+  rewrite falseE; apply: imf_ltsup; exists t => //; apply/eqP.
+  rewrite eq_le supleft andbT sup_upper_bound//.
+  exact/imageP/set_mem.
+pose g t : R := (sup imf - f t)^-1.
+have invf_continuous : {within A, continuous g}.
+  rewrite continuous_subspace_in => t tab; apply: cvgV => //=.
+    by rewrite subr_eq0 gt_eqF // imf_ltsup //; rewrite inE in tab.
+  by apply: cvgD; [exact: cst_continuous | apply: cvgN; exact: (fcont t)].
+have /ex_strict_bound_gt0 [k k_gt0 /= imVfltk] : bounded_set (g @` A).
+  by apply/compact_bounded/continuous_compact.
+have [_ [t tab <-]] : exists2 y, imf y & sup imf - k^-1 < y.
+  by apply: sup_adherent => //; rewrite invr_gt0.
+rewrite ltrBlDr -ltrBlDl.
+suff : sup imf - f t > k^-1 by move=> /ltW; rewrite leNgt => /negbTE ->.
+rewrite -[ltRHS]invrK ltf_pV2// ?qualifE/= ?invr_gt0 ?subr_gt0 ?imf_ltsup//; last first.
+  exact/mem_set.
+by rewrite (le_lt_trans (ler_norm _) _) ?imVfltk//; exact: imageP.
+Qed.
+
+Lemma EVT_min_rV (R : realType) n (f : 'rV[R]_n -> R) (A : set 'rV[R]_n) :
+  A !=set0 ->
+  compact A ->
+  {within A, continuous f} -> exists2 c, c \in A &
+  forall t, t \in A -> f c <= f t.
+Proof.
+move=> A0 cA fcont.
+have /(EVT_max_rV A0 cA) [c clr fcmax] : {within A, continuous (- f)}.
+  by move=> ?; apply: continuousN => ?; exact: fcont.
+by exists c => // ? /fcmax; rewrite lerN2.
+Qed.
+
 Lemma EVT_min (R : realType) (f : R -> R) (a b : R) :
   a <= b -> {within `[a, b], continuous f} -> exists2 c, c \in `[a, b]%R &
   forall t, t \in `[a, b]%R -> f c <= f t.