diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c646e45a7..6730be8bb 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -28,11 +28,11 @@
     `ae_pointwise_almost_uniform`.
 
 - in `exp.v`:
-  + lemmas `power_posrM`, `gt0_ler_power_pos`,
-    `gt0_power_pos`, `norm_power_pos`, `lt0_norm_power_pos`,
-    `power_posB`
-  + lemmas `powere_posrM`, `powere_posAC`, `gt0_powere_pos`,
-    `powere_pos_eqy`, `eqy_powere_pos`, `powere_posD`, `powere_posB`
+  + lemmas `powRrM`, `gt0_ler_powR`,
+    `gt0_powR`, `norm_powR`, `lt0_norm_powR`,
+    `powRB`
+  + lemmas `poweRrM`, `poweRAC`, `gt0_poweR`,
+    `poweR_eqy`, `eqy_poweR`, `poweRD`, `poweRB`
 
 - in `mathcomp_extra.v`:
   + definition `min_fun`, notation `\min`
@@ -41,6 +41,14 @@
 - in `lebesgue_measure.v`:
   + lemmas `measurable_fun_ltr`, `measurable_minr`
 
+- in `exp.v`:
+  + notation `` e `^?(r +? s) ``
+  + lemmas `expR_eq0`, `powRN`
+  + definition `poweRD_def`
+  + lemmas `poweRD_defE`, `poweRB_defE`, `add_neq0_poweRD_def`,
+    `add_neq0_poweRB_def`, `nneg_neq0_poweRD_def`, `nneg_neq0_poweRB_def`
+  + lemmas `powR_eq0`, `poweR_eq0`
+
 ### Changed
 
 - moved from `lebesgue_measure.v` to `real_interval.v`:
@@ -49,20 +57,72 @@
   
 - moved from `functions.v` to `classical_sets.v`: `subsetP`.
 
+- in `exp.v`:
+  + lemmas `power_posD` (now `powRD`), `power_posB` (now `powRB`)
+
 ### Renamed
 
 - in `boolp.v`:
   + `mextentionality` -> `mextensionality`
   + `extentionality` -> `extensionality`
+
 - in `exp.v`:
   + `expK` -> `expRK`
 
+- in `exp.v`:
+  + `power_pos_eq0` -> `powR_eq0_eq0`
+  + `power_pos_inv` -> `powR_invn`
+  + `powere_pos_eq0` -> `poweR_eq0_eq0`
+
+- in `exp.v`:
+  + `power_pos` -> `powR`
+  + `power_pos_ge0` -> `powR_ge0`
+  + `power_pos_gt0` -> `powR_gt0`
+  + `gt0_power_pos` -> `gt0_powR`
+  + `power_pos0` -> `powR0`
+  + `power_posr1` -> `powRr1`
+  + `power_posr0` -> `powRr0`
+  + `power_pos1` -> `powR1`
+  + `ler_power_pos` -> `ler_powR`
+  + `gt0_ler_power_pos` -> `gt0_ler_powR`
+  + `power_posM` -> `powRM`
+  + `power_posrM` -> `powRrM`
+  + `power_posAC` -> `powRAC`
+  + `power_posD` -> `powRD`
+  + `power_posN` -> `powRN`
+  + `power_posB` -> `powRB`
+  + `power_pos_mulrn` -> `powR_mulrn`
+  + `power_pos_inv1` -> `powR_inv1`
+  + `power_pos_intmul` -> `powR_intmul`
+  + `ln_power_pos` -> `ln_powR`
+  + `power12_sqrt` -> `powR12_sqrt`
+  + `norm_power_pos` -> `norm_powR`
+  + `lt0_norm_power_pos` -> `lt0_norm_powR`
+
+- in `lebesgue_measure.v`:
+  + `measurable_power_pos` -> `measurable_powR`
+
+- in `exp.v`:
+  + `powere_pos` -> `poweR`
+  + `powere_pos_EFin` -> `poweR_EFin`
+  + `powere_posyr` -> `poweRyr`
+  + `powere_pose0` -> `poweRe0`
+  + `powere_pose1` -> `poweRe1`
+  + `powere_posNyr` -> `poweRNyr`
+  + `powere_pos0r` -> `poweR0r`
+  + `powere_pos1r` -> `poweR1r`
+  + `fine_powere_pos` -> `fine_poweR`
+  + `powere_pos_ge0` -> `poweR_ge0`
+  + `powere_pos_gt0` -> `poweR_gt0`
+  + `powere_posM` -> `poweRM`
+  + `powere12_sqrt` -> `poweR12_sqrt`
+
 ### Generalized
 
 - in `exp.v`:
-  + lemmas `convex_expR`, `ler_power_pos`
+  + lemmas `convex_expR`, `ler_power_pos` (now `ler_powR`)
 - in `exp.v`:
-  + lemma `ln_power_pos`
+  + lemma `ln_power_pos` (now `ln_powR`)
 
 ### Deprecated
 
diff --git a/classical/all_classical.v b/classical/all_classical.v
index 1d5e0529a..ae1142562 100644
--- a/classical/all_classical.v
+++ b/classical/all_classical.v
@@ -1,7 +1,7 @@
-From mathcomp.classical Require Export boolp.
-From mathcomp.classical Require Export classical_sets.
-From mathcomp.classical Require Export mathcomp_extra.
-From mathcomp.classical Require Export functions.
-From mathcomp.classical Require Export cardinality.
-From mathcomp.classical Require Export fsbigop.
-From mathcomp.classical Require Export set_interval.
+From mathcomp Require Export boolp.
+From mathcomp Require Export classical_sets.
+From mathcomp Require Export mathcomp_extra.
+From mathcomp Require Export functions.
+From mathcomp Require Export cardinality.
+From mathcomp Require Export fsbigop.
+From mathcomp Require Export set_interval.
diff --git a/classical/cardinality.v b/classical/cardinality.v
index bdd89d475..6b3bbbf1b 100644
--- a/classical/cardinality.v
+++ b/classical/cardinality.v
@@ -1,8 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 
 (******************************************************************************)
 (*                              Cardinality                                   *)
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 59356fc30..ad411d925 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
 From mathcomp Require Import ssrint interval.
-From mathcomp.classical Require Import mathcomp_extra boolp.
+From mathcomp Require Import mathcomp_extra boolp.
 
 (******************************************************************************)
 (* This file develops a basic theory of sets and types equipped with a        *)
diff --git a/classical/fsbigop.v b/classical/fsbigop.v
index 231f18d54..23fd1ec38 100644
--- a/classical/fsbigop.v
+++ b/classical/fsbigop.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality.
 
 (******************************************************************************)
 (*                     Finitely-supported big operators                       *)
diff --git a/classical/functions.v b/classical/functions.v
index 264377054..d3045389c 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
 Add Search Blacklist "__canonical__".
 Add Search Blacklist "__functions_".
 Add Search Blacklist "_factory_".
diff --git a/classical/set_interval.v b/classical/set_interval.v
index c03a5b01a..de2125768 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
 From HB Require Import structures.
-From mathcomp.classical Require Import functions.
+From mathcomp Require Import functions.
 
 (******************************************************************************)
 (* This files contains lemmas about sets and intervals.                       *)
diff --git a/theories/Rstruct.v b/theories/Rstruct.v
index 4fdd313f6..fe092e087 100644
--- a/theories/Rstruct.v
+++ b/theories/Rstruct.v
@@ -372,7 +372,7 @@ Canonical R_rcfType := RcfType R Rreal_closed_axiom.
 End ssreal_struct.
 
 Local Open Scope ring_scope.
-From mathcomp.classical Require Import boolp classical_sets.
+From mathcomp Require Import boolp classical_sets.
 Require Import reals.
 
 Section ssreal_struct_contd.
diff --git a/theories/charge.v b/theories/charge.v
index 3d4971696..a77e0e588 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -1,9 +1,8 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.
-From mathcomp.classical Require Import boolp classical_sets cardinality.
-From mathcomp.classical Require Import mathcomp_extra functions fsbigop.
-From mathcomp.classical Require Import set_interval.
+From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality.
+From mathcomp Require Import functions fsbigop set_interval.
 From HB Require Import structures.
 Require Import reals ereal signed topology numfun normedtype sequences.
 Require Import esum measure realfun lebesgue_measure lebesgue_integral.
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index 75b280aa5..9bff25544 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -10,7 +10,7 @@
    incorporate it into mathcomp proper where it could then be used for
    bounds of intervals*)
 From mathcomp Require Import all_ssreflect all_algebra finmap.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra.
 Require Import signed.
 
 (******************************************************************************)
diff --git a/theories/convex.v b/theories/convex.v
index 714ad624d..a7d305092 100644
--- a/theories/convex.v
+++ b/theories/convex.v
@@ -1,10 +1,10 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
 From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
-From mathcomp.classical Require Import boolp classical_sets set_interval.
-From mathcomp.classical Require Import functions cardinality mathcomp_extra.
-Require Import ereal reals signed topology prodnormedzmodule.
-Require Import normedtype derive realfun itv.
+From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
+From mathcomp Require Import functions cardinality.
+Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
+Require Import realfun itv.
 From HB Require Import structures.
 
 (******************************************************************************)
diff --git a/theories/derive.v b/theories/derive.v
index 0d2c3ad4d..f8c0569f8 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -1,7 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import reals signed topology prodnormedzmodule normedtype landau forms.
 
 (******************************************************************************)
diff --git a/theories/ereal.v b/theories/ereal.v
index 3e794dce2..e6be994cb 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -6,8 +6,8 @@
 (* -------------------------------------------------------------------- *)
 
 From mathcomp Require Import all_ssreflect all_algebra finmap.
-From mathcomp.classical Require Import boolp classical_sets functions fsbigop.
-From mathcomp.classical Require Import cardinality set_interval mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import fsbigop cardinality set_interval.
 Require Import reals signed topology.
 Require Export constructive_ereal.
 
diff --git a/theories/esum.v b/theories/esum.v
index 608ae4d23..0d94231d1 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology sequences normedtype numfun.
 
 (******************************************************************************)
diff --git a/theories/exp.v b/theories/exp.v
index 4a2948c06..e48b50696 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import boolp classical_sets functions.
+From mathcomp Require Import mathcomp_extra.
 Require Import reals ereal nsatz_realtype.
 Require Import signed topology normedtype landau sequences derive realfun.
 Require Import itv convex.
@@ -24,6 +24,8 @@ Require Import itv convex.
 (*              e `^ r == power function, in ereal_scope (assumes e >= 0)     *)
 (*          riemannR a == sequence n |-> 1 / (n.+1) `^ a where a has a type   *)
 (*                        of type realType                                    *)
+(*       e `^?(r +? s) == validity condition for the distributivity of        *)
+(*                        the power of the addition, in ereal_scope           *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -36,6 +38,9 @@ Import numFieldNormedType.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
+Reserved Notation "x '`^?' ( r +? s )"
+ (format "x  '`^?' ( r  +?  s )", r at next level, at level 11) .
+
 (* PR to mathcomp in progress *)
 Lemma normr_nneg (R : numDomainType) (x : R) : `|x| \is Num.nneg.
 Proof. by rewrite qualifE. Qed.
@@ -385,6 +390,9 @@ Qed.
 
 Lemma expR_ge0 x : 0 <= expR x. Proof. by rewrite ltW// expR_gt0. Qed.
 
+Lemma expR_eq0 x : (expR x == 0) = false.
+Proof. by rewrite gt_eqF ?expR_gt0. Qed.
+
 Lemma expRN x : expR (- x) = (expR x)^-1.
 Proof.
 apply: (mulfI (lt0r_neq0 (expR_gt0 x))).
@@ -494,7 +502,7 @@ Implicit Types x : R.
 
 Notation exp := (@expR R).
 
-Definition ln x : R := xget 0 [set y | exp y == x ].
+Definition ln x : R := [get y | exp y == x ].
 
 Fact ln0 x : x <= 0 -> ln x = 0.
 Proof.
@@ -595,328 +603,308 @@ Unshelve. all: by end_near. Qed.
 
 End Ln.
 
-Section PowerPos.
+Section PowR.
 Variable R : realType.
 Implicit Types a x : R.
 
-Definition power_pos a x :=
-  if a == 0 then (x == 0)%:R else expR (x * ln a).
+Definition powR a x := if a == 0 then (x == 0)%:R else expR (x * ln a).
 
-Local Notation "a `^ x" := (power_pos a x).
+Local Notation "a `^ x" := (powR a x).
 
-Lemma power_pos_ge0 a x : 0 <= a `^ x.
-Proof. by rewrite /power_pos; case: ifPn => // _; exact: expR_ge0. Qed.
+Lemma powR_ge0 a x : 0 <= a `^ x.
+Proof. by rewrite /powR; case: ifPn => // _; exact: expR_ge0. Qed.
 
-Lemma power_pos_gt0 a x : 0 < a -> 0 < a `^ x.
-Proof. by move=> a0; rewrite /power_pos gt_eqF// expR_gt0. Qed.
+Lemma powR_gt0 a x : 0 < a -> 0 < a `^ x.
+Proof. by move=> a0; rewrite /powR gt_eqF// expR_gt0. Qed.
 
-Lemma gt0_power_pos a x : 0 < x -> 0 <= a -> 0 < a `^ x -> 0 < a.
+Lemma gt0_powR a x : 0 < x -> 0 <= a -> 0 < a `^ x -> 0 < a.
 Proof.
-move=> x0 a0; rewrite /power_pos; case: ifPn => [_|a_neq0 _].
+move=> x0 a0; rewrite /powR; case: ifPn => [_|a_neq0 _].
   by rewrite gt_eqF//= ltxx.
 by rewrite lt_neqAle a0 andbT eq_sym.
 Qed.
 
-Lemma power_pos0 x : x != 0 -> 0 `^ x = 0.
-Proof. by move=> x0; rewrite /power_pos eqxx (negbTE x0). Qed.
+Lemma powR0 x : x != 0 -> 0 `^ x = 0.
+Proof. by move=> x0; rewrite /powR eqxx (negbTE x0). Qed.
 
-Lemma power_posr1 a : 0 <= a -> a `^ 1 = a.
+Lemma powRr1 a : 0 <= a -> a `^ 1 = a.
 Proof.
-rewrite le_eqVlt => /predU1P[<-|a0]; first by rewrite power_pos0// oner_eq0.
-by rewrite /power_pos gt_eqF// mul1r lnK// posrE.
+rewrite le_eqVlt => /predU1P[<-|a0]; first by rewrite powR0// oner_eq0.
+by rewrite /powR gt_eqF// mul1r lnK// posrE.
 Qed.
 
-Lemma power_posr0 a : a `^ 0 = 1.
-Proof. by rewrite /power_pos; case: ifPn; rewrite ?eqxx// mul0r expR0. Qed.
+Lemma powRr0 a : a `^ 0 = 1.
+Proof. by rewrite /powR; case: ifPn; rewrite ?eqxx// mul0r expR0. Qed.
 
-Lemma power_pos1 : power_pos 1 = fun=> 1.
-Proof. by apply/funext => x; rewrite /power_pos oner_eq0 ln1 mulr0 expR0. Qed.
+Lemma powR1 : powR 1 = fun=> 1.
+Proof. by apply/funext => x; rewrite /powR oner_eq0 ln1 mulr0 expR0. Qed.
 
-Lemma power_pos_eq0 x p : x `^ p = 0 -> x = 0.
+Lemma powR_eq0 x p : (x `^ p == 0) = (x == 0) && (p != 0).
 Proof.
-rewrite /power_pos. have [->|_] := eqVneq x 0 => //.
-by move: (expR_gt0 (p * ln x)) => /gt_eqF /eqP.
+rewrite /powR; have [_|x_neq0] := eqVneq x 0 => //.
+  by case: (p == 0); rewrite (oner_eq0, eqxx).
+by rewrite expR_eq0.
 Qed.
 
-Lemma ler_power_pos a : 1 <= a -> {homo power_pos a : x y / x <= y}.
+Lemma powR_eq0_eq0 x p : x `^ p = 0 -> x = 0.
+Proof. by move=> /eqP; rewrite powR_eq0 => /andP[/eqP]. Qed.
+
+Lemma ler_powR a : 1 <= a -> {homo powR a : x y / x <= y}.
 Proof.
 move=> a1 x y xy.
-by rewrite /power_pos gt_eqF ?(lt_le_trans _ a1)// ler_expR ler_wpmul2r ?ln_ge0.
+by rewrite /powR gt_eqF ?(lt_le_trans _ a1)// ler_expR ler_wpmul2r ?ln_ge0.
 Qed.
 
-Lemma gt0_ler_power_pos (r : R) : 0 <= r ->
-  {in `[0, +oo[ &, {homo power_pos ^~ r : x y / x <= y >-> x <= y}}.
+Lemma gt0_ler_powR (r : R) : 0 <= r ->
+  {in `[0, +oo[ &, {homo powR ^~ r : x y / x <= y >-> x <= y}}.
 Proof.
-rewrite le_eqVlt => /predU1P[<- x y _ _ _|]; first by rewrite !power_posr0.
+rewrite le_eqVlt => /predU1P[<- x y _ _ _|]; first by rewrite !powRr0.
 move=> a0 x y; rewrite !in_itv/= !andbT !le_eqVlt => /predU1P[<-|x0].
   move=> /predU1P[<- _|y0 _]; first by rewrite eqxx.
-  by rewrite !power_pos0 ?(gt_eqF a0)// power_pos_gt0 ?orbT.
+  by rewrite !powR0 ?(gt_eqF a0)// powR_gt0 ?orbT.
 move=> /predU1P[<-|y0]; first by rewrite gt_eqF//= ltNge (ltW x0).
 move=> /predU1P[->//|xy]; first by rewrite eqxx.
-by apply/orP; right; rewrite /power_pos !gt_eqF// ltr_expR ltr_pmul2l// ltr_ln.
+by apply/orP; right; rewrite /powR !gt_eqF// ltr_expR ltr_pmul2l// ltr_ln.
 Qed.
 
-Lemma power_posM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
+Lemma powRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
 Proof.
-have [->|r0] := eqVneq r 0; first by rewrite !power_posr0 mulr1.
-rewrite 2!le_eqVlt.
-move=> /predU1P[<-|x0] /predU1P[<-|y0]; rewrite ?(mulr0, mul0r, power_pos0)//.
-- rewrite /power_pos mulf_eq0; case: eqP => [->|x0']/=.
-    rewrite (@gt_eqF _ _ y)//.
-    by case: eqP => /=; rewrite ?mul0r ?mul1r// => ->; rewrite mul0r expR0.
-  by rewrite gt_eqF// lnM ?posrE // -expRD mulrDr.
+rewrite /powR mulf_eq0.
+case: (ltgtP x 0) => // x0 _; case: (ltgtP y 0) => //= y0 _; do ?
+  by case: eqVneq => [r0|]; rewrite ?r0 ?mul0r ?expR0 ?mulr0 ?mul1r.
+by rewrite lnM// mulrDr expRD.
 Qed.
 
-Lemma power_posrM (x y z : R) : x `^ (y * z) = (x `^ y) `^ z.
+Lemma powRrM (x y z : R) : x `^ (y * z) = (x `^ y) `^ z.
 Proof.
-rewrite /power_pos; have [->/=|y0] := eqVneq y 0.
-  by rewrite !mul0r expR0 eqxx/= if_same oner_eq0 ln1 mulr0 expR0.
-have [->/=|z0] := eqVneq z 0.
-  by rewrite !mulr0 !mul0r expR0 eqxx 2!if_same.
-case: ifPn => [_/=|x0]; first by rewrite eqxx mulf_eq0 (negbTE y0) (negbTE z0).
-by rewrite gt_eqF ?expR_gt0// expRK mulrCA mulrA.
+rewrite /powR mulf_eq0; have [_|xN0] := eqVneq x 0.
+  by case: (y == 0); rewrite ?eqxx//= oner_eq0 ln1 mulr0 expR0.
+by rewrite expR_eq0 expRK mulrCA mulrA.
 Qed.
 
-Lemma power_posAC x y z : (x `^ y) `^ z = (x `^ z) `^ y.
-Proof.
-rewrite /power_pos; have [->/=|z0] := eqVneq z 0; rewrite ?mul0r.
-- have [->/=|y0] := eqVneq y 0; rewrite ?mul0r//=.
-  have [x0|x0] := eqVneq x 0; rewrite ?eqxx ?oner_eq0 ?ln1 ?mulr0 ?expR0//.
-  by rewrite oner_eq0 if_same ln1 mulr0 expR0.
-- have [->/=|y0] := eqVneq y 0; rewrite ?mul0r/=.
-    have [x0|x0] := eqVneq x 0; rewrite ?eqxx ?oner_eq0 ?ln1 ?mulr0 ?expR0//.
-    by rewrite oner_eq0 if_same ln1  mulr0 expR0.
-  have [x0|x0] := eqVneq x 0; first by rewrite eqxx.
-  by rewrite gt_eqF ?expR_gt0// gt_eqF ?expR_gt0 ?expRK 1?mulrCA.
-Qed.
-
-Lemma power_posD a : 0 < a -> {morph power_pos a : x y / x + y >-> x * y}.
-Proof. by move=> a0 x y; rewrite /power_pos gt_eqF// mulrDl expRD. Qed.
+Lemma powRAC x y z : (x `^ y) `^ z = (x `^ z) `^ y.
+Proof. by rewrite -!powRrM mulrC. Qed.
 
-Lemma power_posB x r s : r != s -> x `^ (r - s) = x `^ r * x `^ (- s).
+Lemma powRD x r s : (r + s == 0) ==> (x != 0) -> x `^ (r + s) = x `^ r * x `^ s.
 Proof.
-move=> rs.
-have [->|r0] := eqVneq r 0%R; first by rewrite power_posr0 sub0r mul1r.
-have [->|s0] := eqVneq s 0%R; first by rewrite subr0 oppr0 power_posr0 mulr1.
-have [x0|x0|<-] := ltgtP 0 x.
-- by rewrite /power_pos gt_eqF// mulrDl expRD.
-- by rewrite /power_pos lt_eqF// -expRD -mulrDl.
-- by rewrite !power_pos0 ?mulr0// ?subr_eq0// oppr_eq0.
+rewrite /powR; case: (eqVneq x 0) => //= [_|x_neq0 _];
+  last by rewrite mulrDl expRD.
+have [->|] := eqVneq r 0; first by rewrite mul1r add0r.
+by rewrite implybF mul0r => _ /negPf ->.
 Qed.
 
-Lemma power_pos_mulrn a n : 0 <= a -> a `^ n%:R = a ^+ n.
+Lemma powRN x r : x `^ (- r) = (x `^ r)^-1.
 Proof.
-move=> a0; elim: n => [|n ih].
-  by rewrite mulr0n expr0 power_posr0//; apply: lt0r_neq0.
-move: a0; rewrite le_eqVlt => /predU1P[<-|a0].
-  by rewrite !power_pos0 ?mulrn_eq0//= expr0n.
-by rewrite -natr1 power_posD// ih power_posr1// ?exprS 1?mulrC// ltW.
+have [r0|r0] := eqVneq r 0%R; first by rewrite r0 oppr0 powRr0 invr1.
+have [->|xN0] := eqVneq x 0; first by rewrite !powR0 ?oppr_eq0// invr0.
+rewrite -div1r; apply: (canRL (mulfK _)); first by rewrite powR_eq0 (negPf xN0).
+by rewrite -powRD ?addNr ?powRr0// xN0 eqxx.
 Qed.
 
-Lemma power_pos_inv1 a : 0 <= a -> a `^ (-1) = a ^-1.
-Proof.
-rewrite le_eqVlt => /predU1P[<-|a0]; first by rewrite power_pos0// invr0.
-apply/(@mulrI _ a); first by rewrite unitfE gt_eqF.
-rewrite -[X in X * _ = _](power_posr1 (ltW a0)) -power_posD// subrr.
-by rewrite power_posr0 divff// gt_eqF.
-Qed.
+Lemma powRB x r s : (r == s) ==> (x != 0) -> x `^ (r - s) = x `^ r / x `^ s.
+Proof. by move=> ?; rewrite powRD ?subr_eq0// powRN. Qed.
 
-Lemma power_pos_inv a n : 0 <= a -> a `^ (- n%:R) = a ^- n.
+Lemma powR_mulrn a n : 0 <= a -> a `^ n%:R = a ^+ n.
 Proof.
-move=> a0; elim: n => [|n ih].
-  by rewrite -mulNrn mulr0n power_posr0 -exprVn expr0.
-move: a0; rewrite le_eqVlt => /predU1P[<-|a0].
-  by rewrite power_pos0 ?mulrn_eq0// exprnN exp0rz oppr_eq0.
-rewrite -natr1 opprD power_posD// (power_pos_inv1 (ltW a0)) ih.
-by rewrite -[in RHS]exprVn exprS [in RHS]mulrC exprVn.
+move=> a_ge0; elim: n => [|n IHn]; first by rewrite powRr0 expr0.
+by rewrite -natr1 powRD ?natr1 ?pnatr_eq0// powRr1// IHn exprSr.
 Qed.
 
-Lemma power_pos_intmul a (z : int) : 0 <= a -> a `^ z%:~R = a ^ z.
-Proof.
-move=> a0; have [z0|z0] := leP 0 z.
-  rewrite -[in RHS](gez0_abs z0) abszE -exprnP -power_pos_mulrn//.
-  by rewrite natr_absz -abszE gez0_abs.
-rewrite -(opprK z) (_ : - z = `|z|%N); last by rewrite ltz0_abs.
-by rewrite -exprnN -power_pos_inv// nmulrn.
-Qed.
+Lemma powR_inv1 a : 0 <= a -> a `^ (-1) = a ^-1.
+Proof. by move=> a_ge0; rewrite powRN powRr1. Qed.
 
-Lemma ln_power_pos a x : ln (a `^ x) = x * ln a.
+Lemma powR_invn a n : 0 <= a -> a `^ (- n%:R) = a ^- n.
+Proof. by move=> a_ge0; rewrite powRN powR_mulrn. Qed.
+
+Lemma powR_intmul a (z : int) : 0 <= a -> a `^ z%:~R = a ^ z.
+Proof. by move=> a0; case: z => n; [exact: powR_mulrn | exact: powR_invn]. Qed.
+
+Lemma ln_powR a x : ln (a `^ x) = x * ln a.
 Proof.
-have [->|x0] := eqVneq x 0; first by rewrite power_posr0 ln1// mul0r.
-have [->|a0] := eqVneq a 0; first by rewrite power_pos0// ln0// mulr0.
-by rewrite /power_pos (negbTE a0) expRK.
+have [->|x0] := eqVneq x 0; first by rewrite powRr0 ln1// mul0r.
+have [->|a0] := eqVneq a 0; first by rewrite powR0// ln0// mulr0.
+by rewrite /powR (negbTE a0) expRK.
 Qed.
 
-Lemma power12_sqrt a : 0 <= a -> a `^ (2^-1) = Num.sqrt a.
+Lemma powR12_sqrt a : 0 <= a -> a `^ (2^-1) = Num.sqrt a.
 Proof.
 rewrite le_eqVlt => /predU1P[<-|a0].
-  by rewrite power_pos0 ?invr_eq0 ?pnatr_eq0// sqrtr0.
+  by rewrite powR0 ?invr_eq0 ?pnatr_eq0// sqrtr0.
 have /eqP : (a `^ (2^-1)) ^+ 2 = (Num.sqrt a) ^+ 2.
   rewrite sqr_sqrtr; last exact: ltW.
-  by rewrite /power_pos gt_eqF// -expRMm mulrA divrr ?mul1r ?unitfE// lnK.
+  by rewrite /powR gt_eqF// -expRMm mulrA divrr ?mul1r ?unitfE// lnK.
 rewrite eqf_sqr => /predU1P[//|/eqP h].
-have : 0 < a `^ 2^-1 by apply: power_pos_gt0.
+have : 0 < a `^ 2^-1 by exact: powR_gt0.
 by rewrite h oppr_gt0 ltNge sqrtr_ge0.
 Qed.
 
-Lemma norm_power_pos a x : 0 <= a -> `|a `^ x| = `|a| `^ x.
+Lemma norm_powR a x : 0 <= a -> `|a `^ x| = `|a| `^ x.
 Proof.
-move=> a0; rewrite /power_pos; case: ifPn => [/eqP ->|].
+move=> a0; rewrite /powR; case: ifPn => [/eqP ->|].
   by rewrite normr0 eqxx normr_nat.
 rewrite neq_lt ltNge a0/= => {}a0.
 by rewrite gtr0_norm ?expR_gt0// gtr0_norm// gt_eqF.
 Qed.
 
-Lemma lt0_norm_power_pos a x : a < 0 -> `|a `^ x| = 1.
+Lemma lt0_norm_powR a x : a < 0 -> `|a `^ x| = 1.
 Proof.
-move=> a0; rewrite /power_pos lt_eqF// gtr0_norm ?expR_gt0//.
+move=> a0; rewrite /powR lt_eqF// gtr0_norm ?expR_gt0//.
 by rewrite ln0 ?mulr0 ?expR0// ltW.
 Qed.
 
-End PowerPos.
-Notation "a `^ x" := (power_pos a x) : ring_scope.
+End PowR.
+Notation "a `^ x" := (powR a x) : ring_scope.
 
-Section powere_pos.
+Section poweR.
 Local Open Scope ereal_scope.
 Context {R : realType}.
 Implicit Types (s r : R) (x y : \bar R).
 
-Definition powere_pos x r :=
+Definition poweR x r :=
   match x with
   | x'%:E => (x' `^ r)%:E
   | +oo => if r == 0%R then 1%E else +oo
   | -oo => if r == 0%R then 1%E else 0%E
   end.
 
-Local Notation "x `^ r" := (powere_pos x r).
+Local Notation "x `^ r" := (poweR x r).
 
-Lemma powere_pos_EFin s r : s%:E `^ r = (s `^ r)%:E.
+Lemma poweR_EFin s r : s%:E `^ r = (s `^ r)%:E.
 Proof. by []. Qed.
 
-Lemma powere_posyr r : r != 0%R -> +oo `^ r = +oo.
+Lemma poweRyr r : r != 0%R -> +oo `^ r = +oo.
 Proof. by move/negbTE => /= ->. Qed.
 
-Lemma powere_pose0 x : x `^ 0 = 1.
-Proof. by move: x => [x'| |]/=; rewrite ?power_posr0// eqxx. Qed.
+Lemma poweRe0 x : x `^ 0 = 1.
+Proof. by move: x => [x'| |]/=; rewrite ?powRr0// eqxx. Qed.
 
-Lemma powere_pose1 x : 0 <= x -> x `^ 1 = x.
+Lemma poweRe1 x : 0 <= x -> x `^ 1 = x.
 Proof.
-by move: x => [x'| |]//= x0; rewrite ?power_posr1// (negbTE (oner_neq0 _)).
+by move: x => [x'| |]//= x0; rewrite ?powRr1// (negbTE (oner_neq0 _)).
 Qed.
 
-Lemma powere_posNyr r : r != 0%R -> -oo `^ r = 0.
+Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0.
 Proof. by move=> r0 /=; rewrite (negbTE r0). Qed.
 
-Lemma powere_pos_eqy x r : x `^ r = +oo -> x = +oo.
+Lemma poweR_eqy x r : x `^ r = +oo -> x = +oo.
 Proof. by case: x => [x| |] //=; case: ifP. Qed.
 
-Lemma eqy_powere_pos x r : (0 < r)%R -> x = +oo -> x `^ r = +oo.
+Lemma eqy_poweR x r : (0 < r)%R -> x = +oo -> x `^ r = +oo.
 Proof. by move: x => [| |]//= r0 _; rewrite gt_eqF. Qed.
 
-Lemma powere_pos0r r : r != 0%R -> 0 `^ r = 0.
-Proof. by move=> r0; rewrite powere_pos_EFin power_pos0. Qed.
+Lemma poweR0r r : r != 0%R -> 0 `^ r = 0.
+Proof. by move=> r0; rewrite poweR_EFin powR0. Qed.
 
-Lemma powere_pos1r r : 1 `^ r = 1.
-Proof. by rewrite powere_pos_EFin power_pos1. Qed.
+Lemma poweR1r r : 1 `^ r = 1. Proof. by rewrite poweR_EFin powR1. Qed.
 
-Lemma fine_powere_pos x r : fine (x `^ r) = ((fine x) `^ r)%R.
+Lemma fine_poweR x r : fine (x `^ r) = ((fine x) `^ r)%R.
 Proof.
-by move: x => [x| |]//=; case: ifPn => [/eqP ->|?];
-  rewrite ?power_posr0 ?power_pos0.
+by move: x => [x| |]//=; case: ifPn => [/eqP ->|?]; rewrite ?powRr0 ?powR0.
 Qed.
 
-Lemma powere_pos_ge0 x r : 0 <= x `^ r.
-Proof.
-by move: x => [x| |]/=; rewrite ?lee_fin ?power_pos_ge0//; case: ifPn.
-Qed.
+Lemma poweR_ge0 x r : 0 <= x `^ r.
+Proof. by move: x => [x| |]/=; rewrite ?lee_fin ?powR_ge0//; case: ifPn. Qed.
 
-Lemma powere_pos_gt0 x r : 0 < x -> 0 < x `^ r.
+Lemma poweR_gt0 x r : 0 < x -> 0 < x `^ r.
 Proof.
-by move: x => [x|_|]//=; [rewrite lte_fin; exact: power_pos_gt0|case: ifPn].
+by move: x => [x|_|]//=; [rewrite lte_fin; exact: powR_gt0|case: ifPn].
 Qed.
 
-Lemma gt0_powere_pos x r : (0 < r)%R -> 0 <= x -> 0 < x `^ r -> 0 < x.
+Lemma gt0_poweR x r : (0 < r)%R -> 0 <= x -> 0 < x `^ r -> 0 < x.
 Proof.
 move=> r0; move: x => [x|//|]; rewrite ?leeNe_eq// lee_fin !lte_fin.
-exact: gt0_power_pos.
+exact: gt0_powR.
 Qed.
 
-Lemma powere_pos_eq0 x r : -oo < x -> x `^ r = 0 -> x = 0.
+Lemma poweR_eq0 x r : 0 <= x -> (x `^ r == 0) = ((x == 0) && (r != 0%R)).
 Proof.
-move: x => [x _|_/=|//].
-- by rewrite powere_pos_EFin => -[] /power_pos_eq0 ->.
-- by case: ifPn => // _ /eqP; rewrite onee_eq0.
+move: x => [x _|_/=|//]; first by rewrite poweR_EFin eqe powR_eq0.
+by case: ifP => //; rewrite onee_eq0.
 Qed.
 
-Lemma powere_posM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
-Proof.
-move: x y => [x| |] [y| |]//=; first by move=> x0 y0; rewrite -EFinM power_posM.
-- move=> x0 _; case: ifPn => /= [/eqP ->|r0].
-  + by rewrite mule1 power_posr0 powere_pose0.
-  + move: x0; rewrite le_eqVlt => /predU1P[[]<-|/[1!(@lte_fin R)] x0].
-    * by rewrite mul0e powere_pos0r// power_pos0// mul0e.
-    * by rewrite mulry [RHS]mulry !gtr0_sg ?power_pos_gt0// !mul1e powere_posyr.
-- move=> _ y0; case: ifPn => /= [/eqP ->|r0].
-  + by rewrite power_posr0 powere_pose0 mule1.
-  + move: y0; rewrite le_eqVlt => /predU1P[[]<-|/[1!(@lte_fin R)] u0].
-    by rewrite mule0 powere_pos0r// power_pos0// mule0.
-  + by rewrite 2!mulyr !gtr0_sg ?power_pos_gt0// mul1e powere_posyr.
-- move=> _ _; case: ifPn => /= [/eqP ->|r0].
-  + by rewrite powere_pose0 mule1.
-  + by rewrite mulyy powere_posyr.
-Qed.
+Lemma poweR_eq0_eq0 x r : 0 <= x -> x `^ r = 0 -> x = 0.
+Proof. by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed.
 
-Lemma powere_posrM x r s : x `^ (r * s) = (x `^ r) `^ s.
+Lemma poweRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
 Proof.
-case: x => [x| |]/=; first by rewrite power_posrM.
-- have [->|r0] := eqVneq r 0%R; first by rewrite mul0r eqxx powere_pos1r.
-  have [->|s0] := eqVneq s 0%R; first by rewrite mulr0 eqxx powere_pose0.
-  by rewrite mulf_eq0 (negbTE s0) orbF (negbTE r0) ?powere_posyr.
-- have [->|r0] := eqVneq r 0%R; first by rewrite mul0r eqxx powere_pos1r.
-  have [->|s0] := eqVneq s 0%R; first by rewrite mulr0 eqxx powere_pose0.
-  by rewrite mulf_eq0 (negbTE s0) orbF (negbTE r0) powere_pos0r.
+have [->|rN0] := eqVneq r 0%R; first by rewrite !poweRe0 mule1.
+have powyrM s : (0 <= s)%R -> (+oo * s%:E) `^ r = +oo `^ r * s%:E `^ r.
+  case: ltgtP => // [s_gt0 _|<- _]; last first.
+    by rewrite mule0 poweRyr// !poweR0r// mule0.
+  by rewrite gt0_mulye// poweRyr// gt0_mulye// poweR_gt0.
+case: x y => [x| |] [y| |]// x0 y0; first by rewrite /= -EFinM powRM.
+- by rewrite muleC powyrM// muleC.
+- by rewrite powyrM.
+- by rewrite mulyy !poweRyr// mulyy.
 Qed.
 
-Lemma powere_posAC x r s : (x `^ r) `^ s = (x `^ s) `^ r.
+Lemma poweRrM x r s : x `^ (r * s) = (x `^ r) `^ s.
 Proof.
-case: x => [x| |]/=; first by rewrite power_posAC.
-- case: ifPn => [/eqP ->|r0] /=; first by rewrite powere_pose0 power_pos1.
-  by case: ifPn => //; rewrite ?powere_pos1r// powere_posyr.
-case: ifPn => [/eqP ->|r0] /=; first by rewrite power_pos1 powere_pose0.
-case: ifPn => [/eqP ->|s0]; first by rewrite power_posr0 powere_pos1r.
-by rewrite power_pos0// powere_pos0r.
+have [->|s0] := eqVneq s 0%R; first by rewrite mulr0 !poweRe0.
+have [->|r0] := eqVneq r 0%R; first by rewrite mul0r poweRe0 poweR1r.
+case: x => [x| |]//; first by rewrite /= powRrM.
+  by rewrite !poweRyr// mulf_neq0.
+by rewrite !poweRNyr ?poweR0r ?(negPf s0)// mulf_neq0.
 Qed.
 
-Lemma powere_posD x r s : 0 < x -> (0 <= r)%R -> (0 <= s)%R ->
-  x `^ (r + s) = x `^ r * x `^ s.
+Lemma poweRAC x r s : (x `^ r) `^ s = (x `^ s) `^ r.
+Proof. by rewrite -!poweRrM mulrC. Qed.
+
+Definition poweRD_def x r s := ((r + s == 0)%R ==>
+  ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))).
+Notation "x '`^?' ( r +? s )" := (poweRD_def x r s) : ereal_scope.
+
+Lemma poweRD_defE x r s :
+  x `^?(r +? s) = ((r + s == 0)%R ==>
+  ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))).
+Proof. by []. Qed.
+
+Lemma poweRB_defE x r s :
+  x `^?(r +? - s) = ((r == s)%R ==>
+  ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))).
+Proof. by rewrite poweRD_defE subr_eq0 oppr_eq0. Qed.
+
+Lemma add_neq0_poweRD_def x r s : (r + s != 0)%R -> x `^?(r +? s).
+Proof. by rewrite poweRD_defE => /negPf->. Qed.
+
+Lemma add_neq0_poweRB_def x r s : (r != s)%R -> x `^?(r +? - s).
+Proof. by rewrite poweRB_defE => /negPf->. Qed.
+
+Lemma nneg_neq0_poweRD_def x r s : x != 0 -> (r >= 0)%R -> (s >= 0)%R ->
+  x `^?(r +? s).
 Proof.
-move=> x0 r_ge0 s_ge0; move: x0; case: x => [x|_/=|//].
-  by rewrite lte_fin/= => x0; rewrite -EFinM power_posD.
-have [->|r0] := eqVneq r 0%R; first by rewrite mul1e add0r.
-have [->|s0] := eqVneq s 0%R; first by rewrite addr0 (negbTE r0) mule1.
-by rewrite paddr_eq0// (negbTE r0) (negbTE s0) mulyy.
+move=> xN0 rge0 sge0; rewrite /poweRD_def xN0/=.
+by case: ltgtP rge0 => // [r_gt0|<-]; case: ltgtP sge0 => // [s_gt0|<-]//=;
+   rewrite ?addr0 ?add0r ?implybT// gt_eqF//= ?addr_gt0.
 Qed.
 
-Lemma powere_posB x r s : r != s -> x `^ (r - s) = x `^ r * x `^ (- s).
+Lemma nneg_neq0_poweRB_def x r s : x != 0 -> (r >= 0)%R -> (s <= 0)%R ->
+  x `^?(r +? - s).
+Proof. by move=> *; rewrite nneg_neq0_poweRD_def// oppr_ge0. Qed.
+
+Lemma poweRD x r s : x `^?(r +? s) -> x `^ (r + s) = x `^ r * x `^ s.
 Proof.
-move=> rs.
-have [->|r0] := eqVneq r 0%R; first by rewrite powere_pose0 sub0r mul1e.
-have [->|s0] := eqVneq s 0%R; first by rewrite subr0 oppr0 powere_pose0 mule1.
-rewrite /powere_pos.
-case: x => [x| |]/=.
-- by rewrite -EFinM power_posB.
-- by rewrite subr_eq0 (negbTE rs) (negbTE r0) oppr_eq0 (negbTE s0) mulyy.
-- by rewrite subr_eq0 (negbTE rs) (negbTE r0) mul0e.
+rewrite /poweRD_def.
+have [->|r0]/= := eqVneq r 0%R; first by rewrite add0r poweRe0 mul1e.
+have [->|s0]/= := eqVneq s 0%R; first by rewrite addr0 poweRe0 mule1.
+case: x => // [t|/=|/=]; rewrite ?(negPf r0, negPf s0, implybF); last 2 first.
+- by move=> /negPf->; rewrite mulyy.
+- by move=> /negPf->; rewrite mule0.
+rewrite !poweR_EFin eqe => /implyP/(_ _)/andP cnd.
+by rewrite powRD//; apply/implyP => /cnd[].
 Qed.
 
-Lemma powere12_sqrt x : 0 <= x -> x `^ 2^-1 = sqrte x.
+Lemma poweRB x r s : x `^?(r +? - s) -> x `^ (r - s) = x `^ r * x `^ (- s).
+Proof. by move=> rs; rewrite poweRD. Qed.
+
+Lemma poweR12_sqrt x : 0 <= x -> x `^ 2^-1 = sqrte x.
 Proof.
-move: x => [x|_|//]; last by rewrite powere_posyr.
-by rewrite lee_fin => x0 /=; rewrite power12_sqrt.
+move: x => [x|_|//]; last by rewrite poweRyr.
+by rewrite lee_fin => x0 /=; rewrite powR12_sqrt.
 Qed.
 
-End powere_pos.
-Notation "a `^ x" := (powere_pos a x) : ereal_scope.
+End poweR.
+Notation "a `^ x" := (poweR a x) : ereal_scope.
 
 Section riemannR_series.
 Variable R : realType.
@@ -927,15 +915,15 @@ Definition riemannR a : R ^nat := fun n => (n.+1%:R `^ a)^-1.
 Arguments riemannR a n /.
 
 Lemma riemannR_gt0 a i : 0 <= a -> 0 < riemannR a i.
-Proof. by move=> ?; rewrite /riemannR invr_gt0 power_pos_gt0. Qed.
+Proof. by move=> ?; rewrite /riemannR invr_gt0 powR_gt0. Qed.
 
 Lemma dvg_riemannR a : 0 <= a <= 1 -> ~ cvg (series (riemannR a)).
 Proof.
 move=> /andP[a0 a1].
 have : forall n, harmonic n <= riemannR a n.
-  move=> [/=|n]; first by rewrite power_pos1 invr1.
-  rewrite -[leRHS]div1r ler_pdivl_mulr ?power_pos_gt0// mulrC ler_pdivr_mulr//.
-  by rewrite mul1r -[leRHS]power_posr1// (ler_power_pos)// ler1n.
+  move=> [/=|n]; first by rewrite powR1 invr1.
+  rewrite -[leRHS]div1r ler_pdivl_mulr ?powR_gt0// mulrC ler_pdivr_mulr//.
+  by rewrite mul1r -[leRHS]powRr1// (ler_powR)// ler1n.
 move/(series_le_cvg harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))).
 by move/contra_not; apply; exact: dvg_harmonic.
 Qed.
diff --git a/theories/itv.v b/theories/itv.v
index 2603bc611..e8630b0de 100644
--- a/theories/itv.v
+++ b/theories/itv.v
@@ -2,7 +2,7 @@
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
 From mathcomp Require Import interval.
-From mathcomp.classical Require Import boolp mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp.
 Require Import signed.
 
 (******************************************************************************)
diff --git a/theories/kernel.v b/theories/kernel.v
index ae093f87d..66633d079 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality fsbigop.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology normedtype sequences esum measure.
 Require Import numfun lebesgue_measure lebesgue_integral.
 
diff --git a/theories/landau.v b/theories/landau.v
index 5a001ac51..bf550317b 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -1,7 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import ereal reals signed topology normedtype prodnormedzmodule.
 
 (******************************************************************************)
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 1f2fb2a36..8d92615b0 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop .
 Require Import signed reals ereal topology normedtype sequences real_interval.
 Require Import esum measure lebesgue_measure numfun.
 
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 0a6c9ffc9..dd0b3aed1 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology numfun normedtype.
 From HB Require Import structures.
 Require Import sequences esum measure real_interval realfun exp.
@@ -1650,7 +1650,7 @@ rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first.
   by rewrite -(setCitv `[0, 0]); apply/seteqP; split => [|]x/=;
     rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP].
 apply/measurable_funU => //; split.
-- apply/(@measurable_restrict _ _ _ _ _ setT) => //. 
+- apply/(@measurable_restrict _ _ _ _ _ setT) => //.
   rewrite (_ : _ \_ _ = cst (0:R))//; apply/funext => y; rewrite patchE.
   by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW.
 - have : {in `]0, +oo[%classic, continuous (@ln R)}.
@@ -1668,8 +1668,8 @@ Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed.
 #[global] Hint Extern 0 (measurable_fun _ expR) =>
   solve [apply: measurable_expR] : core.
 
-Lemma measurable_power_pos (R : realType) p :
-  measurable_fun [set: R] (@power_pos R ^~ p).
+Lemma measurable_powR (R : realType) p :
+  measurable_fun [set: R] (@powR R ^~ p).
 Proof.
 apply: measurable_fun_if => //.
 - apply: (measurable_fun_bool true); rewrite (_ : _ @^-1` _ = [set 0])//.
@@ -1678,10 +1678,12 @@ apply: measurable_fun_if => //.
   rewrite (_ : _ @^-1` _ = [set~ 0]); first exact: measurableT_comp.
   by apply/seteqP; split => [x /negP/negP/eqP|x x0]//=; exact/negbTE/eqP.
 Qed.
-#[global] Hint Extern 0 (measurable_fun _ (@power_pos _ ^~ _)) =>
-  solve [apply: measurable_power_pos] : core.
-#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_power_pos` instead")]
-Notation measurable_fun_power_pos := measurable_power_pos.
+#[global] Hint Extern 0 (measurable_fun _ (@powR _ ^~ _)) =>
+  solve [apply: measurable_powR] : core.
+#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_powR` instead")]
+Notation measurable_fun_power_pos := measurable_powR.
+#[deprecated(since="mathcomp-analysis 0.6.4", note="use `measurable_powR` instead")]
+Notation measurable_power_pos := measurable_powR.
 #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")]
 Notation measurable_fun_max := measurable_maxr.
 
@@ -1870,7 +1872,7 @@ Lemma lebesgue_regularity_outer (D : set R) (eps : R) :
 Proof.
 move=> mD muDpos epspos.
 have /ereal_inf_lt[z [/= M' covDM sMz zDe]] : mu D < mu D + (eps / 2)%:E.
-  by rewrite lte_spaddr ?lte_fin ?divr_gt0// ge0_fin_numE.
+  by rewrite lte_spaddre ?lte_fin ?divr_gt0// ge0_fin_numE.
 pose e2 n := (eps / 2) / (2 ^ n.+1)%:R.
 have e2pos n : (0 < e2 n)%R by rewrite ?divr_gt0.
 pose M n := if pselect (M' n = set0) then set0 else
@@ -2013,23 +2015,23 @@ Context (mu : {measure set T -> \bar R}).
 Local Open Scope ereal_scope.
 
 (*TODO : this generalizes to any metric space with a borel measure*)
-Lemma pointwise_almost_uniform 
+Lemma pointwise_almost_uniform
     (f_ : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R):
   (forall n, measurable_fun A (f_ n)) -> measurable_fun A g ->
   measurable A -> mu A < +oo -> (forall x, A x -> f_ ^~ x --> g x) ->
-  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E & 
+  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
     {uniform A `\` B, f_ --> g}].
 Proof.
 move=> mf mg mA finA fptwsg epspos; pose h q (z : T) : R := `|f_ q z - g z|%R.
 have mfunh q : measurable_fun A (h q).
   by apply: measurableT_comp; [exact: measurable_normr |exact: measurable_funB].
-pose E k n := \bigcup_(i in [set j : nat | (n <= j)%N ]) 
+pose E k n := \bigcup_(i in [set j : nat | (n <= j)%N ])
   (A `&` [set x | (h i x >= k.+1%:R^-1)%R]).
-have Einc k : nonincreasing_seq (E k). 
-  move=> n m nm; apply/asboolP => z [i] /= /(leq_trans _) mi [? ?]. 
+have Einc k : nonincreasing_seq (E k).
+  move=> n m nm; apply/asboolP => z [i] /= /(leq_trans _) mi [? ?].
   by exists i => //; apply: mi.
-have mE k n : measurable (E k n). 
-  apply: bigcup_measurable => q /= ?. 
+have mE k n : measurable (E k n).
+  apply: bigcup_measurable => q /= ?.
   have -> : [set x | h q x >= k.+1%:R^-1]%R = (h q)@^-1` (`[k.+1%:R^-1, +oo[).
     by rewrite eqEsubset; split => z; rewrite /= in_itv /= Bool.andb_true_r.
   exact: mfunh.
@@ -2040,8 +2042,8 @@ have nEcvg x k : exists n, A x -> (~` (E k n)) x.
     have ki0 : ((0:R) < k.+1%:R^-1)%R by rewrite invr_gt0.
     rewrite (_ : k.+1%:R^-1 = (PosNum ki0)%:num ) //; exact: nbhsx_ballx.
   move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni.
-  apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC. 
-  case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center.
+  apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC.
+  by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center.
 have Ek0 k : (\bigcap_n (E k n)) = set0.
   rewrite eqEsubset; split => // z /=; suff : (~` \bigcap_n E k n) z by done.
   rewrite setC_bigcap; case : (pselect (A z)) => [Az | nAz].
@@ -2050,24 +2052,24 @@ have Ek0 k : (\bigcap_n (E k n)) = set0.
 have badn' : forall k, exists n, mu (E k n) < ((eps/2) / (2 ^ k.+1)%:R)%:E.
   move=> k; pose ek :R := eps/2 / (2 ^ k.+1)%:R; have : mu \o E k --> (0%R)%:E.
     rewrite -(measure0 mu) -(Ek0 k); apply: nonincreasing_cvg_mu => //.
-    - apply: (le_lt_trans _ finA); apply: le_measure; rewrite ?inE //. 
+    - apply: (le_lt_trans _ finA); apply: le_measure; rewrite ?inE //.
       by move=> ? [? _ []].
     - by apply: bigcap_measurable => ?.
   case/fine_cvg/(_ (interior (ball (0:R) ek))%R).
     apply: open_nbhs_nbhs; split; first exact: open_interior.
     have ekpos : (0 < ek)%R by rewrite divr_gt0 // divr_gt0.
     by move: ek ekpos => _/posnumP[ek]; exact: nbhsx_ballx.
-  move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN. 
+  move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN.
   rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//.
   by apply:(le_lt_trans _ finA); apply le_measure; rewrite ?inE// => ? [? _ []].
 pose badn k := projT1 (cid (badn' k)); exists (\bigcup_k (E k (badn k))); split.
 - exact: bigcup_measurable.
 - apply: (@le_lt_trans _ _ (eps/2)%R%:E); first last.
     by rewrite lte_fin ltr_pdivr_mulr // ltr_pmulr // Rint_ltr_addr1 // ?Rint1.
-  apply: le_trans. 
+  apply: le_trans.
     apply: (measure_sigma_sub_additive _ (fun k => mE k (badn k)) _ _) => //.
     exact: bigcup_measurable.
-  apply: le_trans; first last. 
+  apply: le_trans; first last.
     by apply: (@epsilon_trick0 R _ xpredT); rewrite divr_ge0 //; exact: ltW.
   by rewrite lee_nneseries // => n _; exact/ltW/(projT2 (cid (badn' _))).
 apply/uniform_restrict_cvg => /= U /=; rewrite ?uniform_nbhsT.
@@ -2080,15 +2082,15 @@ rewrite /E setC_bigcup => /(_ (r)) /=; rewrite /h => /(_ badNr) /not_andP [] //.
 by move/negP; rewrite real_ltNge // distrC.
 Qed.
 
-Lemma ae_pointwise_almost_uniform 
+Lemma ae_pointwise_almost_uniform
     (f_ : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R):
   (forall n, measurable_fun A (f_ n)) -> measurable_fun A g ->
   measurable A -> mu A < +oo -> {ae mu, (forall x, A x -> f_ ^~ x --> g x)} ->
-  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E & 
+  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
     {uniform A `\` B, (fun n => (f_ n : T -> R)) --> g}].
 Proof.
 move=> mf mg mA Afin [C [mC C0 nC] epspos].
-have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E & 
+have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E &
     {uniform (A `\` C) `\` B,  f_ --> g}].
   apply: pointwise_almost_uniform => //.
   - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? [].
@@ -2100,7 +2102,7 @@ have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E &
 exists (B `|` C); split.
 - exact: measurableU.
 - by apply: (le_lt_trans _ Beps); rewrite measureU0.
-- by rewrite setUC -setDDl. 
+- by rewrite setUC -setDDl.
 Qed.
 
-End egorov.
\ No newline at end of file
+End egorov.
diff --git a/theories/measure.v b/theories/measure.v
index a49721cf0..9c232b84a 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect all_algebra finmap.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop .
 Require Import reals ereal signed topology normedtype sequences esum numfun.
 From HB Require Import structures.
 
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 973712290..c26abcb60 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
 From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality set_interval mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality set_interval.
 Require Import ereal reals signed topology prodnormedzmodule.
 
 (******************************************************************************)
diff --git a/theories/nsatz_realtype.v b/theories/nsatz_realtype.v
index 85d83307c..00be33ae9 100644
--- a/theories/nsatz_realtype.v
+++ b/theories/nsatz_realtype.v
@@ -1,6 +1,6 @@
 Require Import Nsatz.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum.
-From mathcomp.classical Require Import boolp.
+From mathcomp Require Import boolp.
 Require Import reals ereal.
 
 (******************************************************************************)
diff --git a/theories/numfun.v b/theories/numfun.v
index f8a09cdf8..39caa9a96 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -1,9 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
-From mathcomp Require Import ssralg ssrnum ssrint interval finmap.
-From mathcomp.classical Require Import boolp classical_sets fsbigop.
-From mathcomp.classical Require Import functions cardinality mathcomp_extra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
+From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop.
+From mathcomp Require Import functions cardinality .
 Require Import signed reals ereal topology normedtype sequences.
 
 (******************************************************************************)
diff --git a/theories/probability.v b/theories/probability.v
index 4ad5fd95b..9919b1a45 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality.
 From HB Require Import structures.
 Require Import reals ereal signed topology normedtype sequences esum measure.
 Require Import exp numfun lebesgue_measure lebesgue_integral.
diff --git a/theories/real_interval.v b/theories/real_interval.v
index 7b00c7dbb..b22f52486 100644
--- a/theories/real_interval.v
+++ b/theories/real_interval.v
@@ -1,9 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
-From mathcomp.classical Require Export set_interval.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Export set_interval.
 From HB Require Import structures.
 Require Import reals ereal signed topology normedtype sequences.
 
diff --git a/theories/realfun.v b/theories/realfun.v
index f71c9af02..0ac63a572 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -1,10 +1,10 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
 From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
-From mathcomp.classical Require Import boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality mathcomp_extra.
-Require Import ereal reals signed topology prodnormedzmodule.
-Require Import normedtype derive real_interval.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality.
+Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
+Require Import real_interval.
 From HB Require Import structures.
 
 (******************************************************************************)
diff --git a/theories/reals.v b/theories/reals.v
index 61cc81742..248f65307 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -36,8 +36,7 @@
 (******************************************************************************)
 
 From mathcomp Require Import all_ssreflect all_algebra.
-From mathcomp.classical Require Import boolp classical_sets set_interval.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
 
 Require Import Setoid.
 
diff --git a/theories/sequences.v b/theories/sequences.v
index ca523a67c..59f210c6a 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
-From mathcomp.classical Require Import boolp classical_sets.
-From mathcomp.classical Require Import functions set_interval mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import set_interval.
 Require Import reals ereal signed topology normedtype landau.
 
 (******************************************************************************)
diff --git a/theories/signed.v b/theories/signed.v
index 5f56ab8dc..f8e4c64f2 100644
--- a/theories/signed.v
+++ b/theories/signed.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra.
 
 (******************************************************************************)
 (* This file develops tools to make the manipulation of numbers with a known  *)
diff --git a/theories/summability.v b/theories/summability.v
index 1f9287723..0ed596ee5 100644
--- a/theories/summability.v
+++ b/theories/summability.v
@@ -2,9 +2,8 @@
 Require Reals.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
 From mathcomp Require Import interval zmodp.
-From mathcomp.classical Require Import boolp classical_sets.
-Require Import ereal reals.
-Require Import Rstruct signed topology normedtype.
+From mathcomp Require Import boolp classical_sets.
+Require Import ereal reals Rstruct signed topology normedtype.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/topology.v b/theories/topology.v
index 1ba1896c8..66c42a765 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality mathcomp_extra fsbigop.
+From mathcomp Require Import boolp classical_sets functions.
+From mathcomp Require Import cardinality mathcomp_extra fsbigop.
 Require Import reals signed.
 
 (******************************************************************************)
diff --git a/theories/trigo.v b/theories/trigo.v
index 80ac45e1c..b1809ffba 100644
--- a/theories/trigo.v
+++ b/theories/trigo.v
@@ -1,8 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import reals ereal nsatz_realtype signed topology normedtype landau.
 Require Import sequences derive realfun exp.