diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 5025f4d491..0b121325d1 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -38,7 +38,7 @@
     `exp_funD`, `exp_fun_inv`, `exp_fun_mulrn`
   + definition `riemannR`, lemmas `riemannR_gt0`, `dvg_riemannR`
 - new file `trigo.v`
-  + lemmas `sqrtvR`, `divr_eq`, `sum_group`, `cvg_series_cvg_series_group`,
+  + lemmas `sqrtvR`, `eqr_div`, `big_nat_mul`, `cvg_series_cvg_series_group`,
     `cvg_series_cvg_series_group2`, `lt_sum_lim_series`
   + definitions `periodic`, `alternating`
   + lemmas `periodicn`, `alternatingn`
diff --git a/theories/exp.v b/theories/exp.v
index 504de1eee6..95b19cf5d2 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -4,7 +4,7 @@ From mathcomp Require Import matrix interval rat.
 Require Import boolp reals ereal.
 Require Import nsatz_realtype.
 Require Import classical_sets posnum topology normedtype landau sequences.
-Require Import derive continuous_inverse.
+Require Import derive inverse_continuous.
 
 (******************************************************************************)
 (*               Theory of exponential/logarithm functions                    *)
diff --git a/theories/trigo.v b/theories/trigo.v
index 06be2b4bbf..98153761a7 100644
--- a/theories/trigo.v
+++ b/theories/trigo.v
@@ -38,6 +38,7 @@ Import numFieldNormedType.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
+(* NB: packport to mathcomp in progress *)
 Lemma sqrtrV (R : rcfType) (x : R) : 0 <= x -> Num.sqrt (x^-1) = (Num.sqrt x)^-1.
 Proof.
 move=> x_ge0.
@@ -47,7 +48,7 @@ rewrite -[LHS]mul1r -(mulVf (_ : Num.sqrt x != 0)); last first.
 by rewrite -mulrA -sqrtrM // divff // sqrtr1 mulr1.
 Qed.
 
-Lemma divr_eq (R : numFieldType) (x y z t : R):
+Lemma eqr_div (R : numFieldType) (x y z t : R):
   y != 0 -> t != 0 -> (x / y == z / t) = (x * t == z * y).
 Proof.
 move=> yD0 tD0.
@@ -56,29 +57,32 @@ apply/eqP/eqP=> [->//|H].
 by apply/(mulIf tD0)/(mulIf yD0).
 Qed.
 
-Lemma sum_group (R : zmodType) (f : R ^nat) (n k : nat) :
-  \sum_(0 <= i < n) \sum_(i * k <= j < i.+1 * k) f j =
-  \sum_(0 <= i < n * k) f i.
+Lemma big_nat_mul (R : zmodType) (f : R ^nat) (n k : nat) :
+  \sum_(0 <= i < n * k) f i =
+  \sum_(0 <= i < n) \sum_(i * k <= j < i.+1 * k) f j.
 Proof.
 elim: n => [|n ih]; first by rewrite mul0n 2!big_nil.
-rewrite big_nat_recr//= ih mulSn addnC [in RHS]/index_iota subn0 iota_add.
-rewrite big_cat /= [in X in X + _ = _]/index_iota subn0; congr (_ + _).
-by rewrite /index_iota addnC addnK.
+rewrite [in RHS]big_nat_recr//= -ih mulSn addnC [in LHS]/index_iota subn0 iotaD.
+rewrite big_cat /= [in X in _ = X  _]/index_iota subn0; congr (_ + _).
+by rewrite add0n /index_iota (addnC _ k) addnK.
 Qed.
+(* /NB: packport to mathcomp in progress *)
 
-Lemma cvg_series_cvg_series_group (R : realFieldType) (f : R ^nat) k : cvg (series f) -> (0 < k)%N ->
+Lemma cvg_series_cvg_series_group (R : realFieldType) (f : R ^nat) k :
+  cvg (series f) -> (0 < k)%N ->
   series (fun n => \sum_(n * k <= i < n.+1 * k) f i) --> lim (series f).
 Proof.
 move=> /cvg_ballP cf k0; apply/cvg_ballP => _/posnumP[e].
 have := cf _ (posnum_gt0 e); rewrite near_map => -[n _ nl].
 rewrite near_map; near=> m.
-rewrite /ball /= [in X in `|_ - X|]/series [in X in `|_ - X|]/= sum_group.
+rewrite /ball /= [in X in `|_ - X|]/series [in X in `|_ - X|]/= -big_nat_mul.
 have /nl : (n <= m * k)%N.
   by near: m; exists n.+1 => //= p /ltnW /leq_trans /(_ (leq_pmulr _ k0)).
 by rewrite /ball /= distrC.
 Grab Existential Variables. all: end_near. Qed.
 
-Lemma cvg_series_cvg_series_group2 (R : realFieldType) (f : R ^nat) : cvg (series f) ->
+Lemma cvg_series_cvg_series_group2 (R : realFieldType) (f : R ^nat) :
+  cvg (series f) ->
   series (fun n => \sum_(n.*2 <= i < n.*2 + 2) f i) --> lim (series f).
 Proof.
 move=> cf; rewrite [X in series X --> _](_ : _ =