diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 8a3179698e..9fb2eb02cb 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -9,6 +9,14 @@
 
 - in `realfun.v`:
   + instance `is_derive1_sqrt`
+- in `mathcomp_extra.v`:
+  + lemmas `subrKC`, `sumr_le0`, `card_fset_sum1`
+
+- in `functions.v`:
+  + lemmas `fct_prodE`, `prodrfctE`
+
+- in `exp.v:
+  + lemma `norm_expR`
 
 ### Changed
 
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 44ff437757..796d671fec 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -1518,7 +1518,7 @@ Proof. by case=> [t ?]; exists (f t). Qed.
 Lemma preimage_image f A : A `<=` f @^-1` (f @` A).
 Proof. by move=> a Aa; exists a. Qed.
 
-Lemma preimage_range {A B : Type} (f : A -> B) : f @^-1` (range f) = [set: A].
+Lemma preimage_range f : f @^-1` (range f) = [set: aT].
 Proof. by rewrite eqEsubset; split=> x // _; exists x. Qed.
 
 Lemma image_preimage_subset f Y : f @` (f @^-1` Y) `<=` Y.
diff --git a/classical/functions.v b/classical/functions.v
index feecd8eb83..0209089651 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2652,6 +2652,11 @@ Lemma fct_sumE (I T : Type) (M : nmodType) r (P : {pred I}) (f : I -> T -> M) :
   \sum_(i <- r | P i) f i = fun x => \sum_(i <- r | P i) f i x.
 Proof. by apply/funext => ?; elim/big_rec2: _ => //= i y ? Pi <-. Qed.
 
+Lemma fct_prodE (I : Type) (T : pointedType) (M : ringType) r (P : {pred I})
+    (f : I -> T -> M) :
+  \prod_(i <- r | P i) f i = fun x => \prod_(i <- r | P i) f i x.
+Proof. by apply/funext => ?; elim/big_rec2: _ => //= i y ? Pi <-. Qed.
+
 Lemma mul_funC (T : Type) {R : comSemiRingType} (f : T -> R) (r : R) :
   r \*o f = r \o* f.
 Proof. by apply/funext => x/=; rewrite mulrC. Qed.
@@ -2670,6 +2675,10 @@ Lemma sumrfctE (T : Type) (K : nmodType) (s : seq (T -> K)) :
   \sum_(f <- s) f = (fun x => \sum_(f <- s) f x).
 Proof. exact: fct_sumE. Qed.
 
+Lemma prodrfctE (T : pointedType) (K : ringType) (s : seq (T -> K)) :
+  \prod_(f <- s) f = (fun x => \prod_(f <- s) f x).
+Proof. exact: fct_prodE. Qed.
+
 Lemma natmulfctE (U : Type) (K : nmodType) (f : U -> K) n :
   f *+ n = (fun x => f x *+ n).
 Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed.
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 6245db399c..2e7d9f38ec 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -470,3 +470,21 @@ Proof. by move=>  ? ? []. Qed.
 
 Lemma inl_inj {A B} : injective (@inl A B).
 Proof. by move=>  ? ? []. Qed.
+
+(**************************)
+(* MathComp 2.5 additions *)
+(**************************)
+
+Section ssralg.
+Lemma subrKC {V : zmodType} (x y : V) : x + (y - x) = y.
+Proof. by rewrite addrC subrK. Qed.
+End ssralg.
+
+Lemma sumr_le0 (R : numDomainType) I (r : seq I) (P : pred I) (F : I -> R) :
+  (forall i, P i -> F i <= 0)%R -> (\sum_(i <- r | P i) F i <= 0)%R.
+Proof. by move=> F0; elim/big_rec : _ => // i x Pi; apply/ler_wnDl/F0. Qed.
+
+(* to appear in coq-mathcomp-finmap > 2.2.1 *)
+Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) :
+  #|` A| = (\sum_(i <- A) 1)%N.
+Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed.
diff --git a/classical/unstable.v b/classical/unstable.v
index 159013ef15..d8d72d0a11 100644
--- a/classical/unstable.v
+++ b/classical/unstable.v
@@ -35,11 +35,6 @@ Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
-Section ssralg.
-Lemma subrKC {V : zmodType} (x y : V) : x + (y - x) = y.
-Proof. by rewrite addrC subrK. Qed.
-End ssralg.
-
 (* NB: Coq 8.17.0 generalizes dependent_choice from Set to Type
    making the following lemma redundant *)
 Section dependent_choice_Type.
@@ -164,10 +159,6 @@ Qed.
 End path_lt.
 Arguments last_filterP {d T a} P s.
 
-Lemma sumr_le0 (R : numDomainType) I (r : seq I) (P : pred I) (F : I -> R) :
-  (forall i, P i -> F i <= 0)%R -> (\sum_(i <- r | P i) F i <= 0)%R.
-Proof. by move=> F0; elim/big_rec : _ => // i x Pi; apply/ler_wnDl/F0. Qed.
-
 Inductive boxed T := Box of T.
 
 Reserved Notation "`1- r" (format "`1- r", at level 2).
@@ -192,10 +183,6 @@ have [i _ /(_ _ isT) mf] := @arg_maxnP _ (@ord0 n) xpredT f isT.
 by exists i; split; rewrite ?leq_ord// => j jn; have := mf (@Ordinal n.+1 j jn).
 Qed.
 
-Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) :
-  #|` A| = (\sum_(i <- A) 1)%N.
-Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed.
-
 Arguments big_rmcond {R idx op I r} P.
 Arguments big_rmcond_in {R idx op I r} P.
 
@@ -411,7 +398,7 @@ Qed.
 
 End FsetPartitions.
 
-(* TODO: move to ssrnum *)
+(* PR 1420 to MathComp in progress *)
 Lemma prodr_ile1 {R : realDomainType} (s : seq R) :
   (forall x, x \in s -> 0 <= x <= 1)%R -> (\prod_(j <- s) j <= 1)%R.
 Proof.
@@ -423,11 +410,11 @@ rewrite mulr_ile1 ?andbT//.
 by rewrite ih// => e xs; rewrite xs01// in_cons xs orbT.
 Qed.
 
-(* TODO: move to ssrnum *)
-
+(* PR 1420 to MathComp in progress *)
 Lemma size_filter_gt0 T P (r : seq T) : (size (filter P r) > 0)%N = (has P r).
 Proof. by elim: r => //= x r; case: ifP. Qed.
 
+(* PR 1420 to MathComp in progress *)
 Lemma ltr_sum [R : numDomainType] [I : Type] (r : seq I)
     [P : pred I] [F G : I -> R] :
   has P r ->
@@ -440,6 +427,7 @@ rewrite !big_cons ltr_leD// ?ltFG// -(all_filterP Pr) !big_filter.
 by rewrite ler_sum => // i Pi; rewrite ltW ?ltFG.
 Qed.
 
+(* PR 1420 to MathComp in progress *)
 Lemma ltr_sum_nat [R : numDomainType] [m n : nat] [F G : nat -> R] :
   (m < n)%N -> (forall i : nat, (m <= i < n)%N -> F i < G i) ->
   \sum_(m <= i < n) F i < \sum_(m <= i < n) G i.
@@ -448,7 +436,6 @@ move=> lt_mn i; rewrite big_nat [ltRHS]big_nat ltr_sum//.
 by apply/hasP; exists m; rewrite ?mem_index_iota leqnn lt_mn.
 Qed.
 
-
 Lemma eq_exists2l (A : Type) (P P' Q : A -> Prop) :
   (forall x, P x <-> P' x) ->
   (exists2 x, P x & Q x) <-> (exists2 x, P' x & Q x).
diff --git a/theories/exp.v b/theories/exp.v
index 819e5713d9..f1358bd12a 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -410,6 +410,9 @@ Qed.
 
 Lemma expR_ge0 x : 0 <= expR x. Proof. by rewrite ltW// expR_gt0. Qed.
 
+Lemma norm_expR : normr \o expR = (expR : R -> R).
+Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed.
+
 Lemma expR_eq0 x : (expR x == 0) = false.
 Proof. by rewrite gt_eqF ?expR_gt0. Qed.