diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c3166b5229..fdde6ee25f 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -26,6 +26,10 @@
 - in `lebesgue_integral_approximation.v`:
   + lemma `measurable_prod`
 
+- in `exp.v`:
+  + lemmas `lnNy`, `powR_cvg0`, `derivable_powR`, `powR_derive1`
+  + Instance `is_derive1_powR`
+
 ### Changed
 
 - in `pi_irrational`:
@@ -38,6 +42,9 @@
 
 ### Generalized
 
+- in `normedtype.v`:
+  + lemmas `gt0_cvgMlNy`, `gt0_cvgMly`
+
 ### Deprecated
 
 ### Removed
diff --git a/theories/exp.v b/theories/exp.v
index 230b3c1abf..ac49403b13 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -790,6 +790,12 @@ by rewrite !lnK// -(@ler_ln) ?posrE ?expR_gt0 ?conv_gt0// expRK.
 Qed.
 Local Close Scope convex_scope.
 
+Lemma lnNy : ln x @[x --> 0^'+] --> -oo.
+Proof.
+apply/cvgrNyPle => y; near=> x; rewrite -ler_expR lnK; last by rewrite posrE.
+by near: x; apply: nbhs_right_le; exact: expR_gt0.
+Unshelve. end_near. Qed.
+
 End Ln.
 
 Section PowR.
@@ -1053,6 +1059,52 @@ Qed.
 Canonical powR_inum (i : Itv.t) (x : Itv.def (@Itv.num_sem R) i) p :=
   Itv.mk (num_spec_powR x p).
 
+Lemma powR_cvg0 (x : R) : 0 < x -> a `^ x @[a --> 0^'+] --> 0.
+Proof.
+move=> x0; apply: (@cvg_trans _ ((expR (ln a * x)) @[a --> 0^'+])).
+  by apply: near_eq_cvg; near=> a; rewrite /powR gt_eqF 1?mulrC.
+apply: (@cvg_comp _ _ _ _ _ _ (@ninfty_nbhs R)).
+  by apply: gt0_cvgMlNy; rewrite ?x0//; exact: lnNy.
+exact/cvgNy_compNP/cvgr_expR.
+Unshelve. end_near. Qed.
+
+Lemma derivable_powR v x : v != 0 ->
+  {in `]0, +oo[, forall a, derivable (powR ^~ x) a v}.
+Proof.
+move=> v0 a; rewrite in_itv/= andbT => a0.
+apply: (@near_eq_derivable _ _ _ (fun a' => expR (x * ln a'))) => //.
+  by near=> b; rewrite /powR gt_eqF//; near: b; exact: lt_nbhsr.
+apply: diff_derivable; apply: differentiable_comp; last exact/derivable1_diffP.
+apply: differentiableM => //; apply/derivable1_diffP.
+by apply: ex_derive; exact: is_derive1_ln.
+Unshelve. end_near. Qed.
+
+Lemma powR_derive1 a : {in `]0, +oo[%R,
+  (powR ^~ a) ^`()%classic =1 (fun x => a * x `^ (a - 1))}.
+Proof.
+move=> x; rewrite in_itv/= andbT => x0.
+rewrite derive1E.
+rewrite (@near_eq_derive _ _ _ _ (fun x => expR (a * ln x)))//; last first.
+  by near=> z; rewrite /powR gt_eqF//; near: z; exact: lt_nbhsr.
+rewrite -derive1E.
+rewrite derive1_comp//=; last first.
+  by apply: derivableM => //; apply: ex_derive; exact: is_derive1_ln.
+rewrite 2!derive1E.
+rewrite deriveM//; last by apply: ex_derive; exact: is_derive1_ln.
+rewrite !derive_val scaler0 addr0.
+have [_ ->] := (is_derive1_ln x0).
+rewrite mulrC powRB; last by rewrite (@gt_eqF _ _ x)//; apply: implybT.
+by rewrite powRr1 ?ltW// mulrA [in RHS]mulrAC /powR gt_eqF.
+Unshelve. end_near. Qed.
+
+Global Instance is_derive1_powR (a x : R) : 0 < x ->
+  is_derive x 1 (powR ^~ a) (a * x `^ (a - 1))%R.
+Proof.
+move=> x_gt0; split.
+  by apply: derivable_powR; rewrite ?in_itv/= ?andbT.
+by rewrite -derive1E powR_derive1// in_itv andbT.
+Qed.
+
 End PowR.
 Notation "a `^ x" := (powR a x) : ring_scope.
 
diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v
index 08b8eec1d6..1527b46943 100644
--- a/theories/normedtype_theory/num_normedtype.v
+++ b/theories/normedtype_theory/num_normedtype.v
@@ -505,19 +505,20 @@ rewrite pmulrn ceil_le_int// [ceil _]intEsign.
 by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo.
 Unshelve. all: by end_near. Qed.
 
-Lemma gt0_cvgMlNy {R : realFieldType} (M : R) (f : R -> R) : (0 < M)%R ->
-  (f r) @[r --> -oo] --> -oo -> (f r * M)%R @[r --> -oo] --> -oo.
+Lemma gt0_cvgMlNy {R : realFieldType} {F : set_system R} {FF : Filter F} (M : R)
+  (f : R -> R) :
+  (0 < M)%R -> (f r) @[r --> F] --> -oo -> (f r * M)%R @[r --> F] --> -oo.
 Proof.
 move=> M0 /cvgrNyPle fy; apply/cvgrNyPle => A.
 by apply: filterS (fy (A / M)) => x; rewrite ler_pdivlMr.
 Qed.
 
-Lemma gt0_cvgMly {R : realFieldType} (M : R) (f : R -> R) : (0 < M)%R ->
-  f r @[r --> +oo] --> +oo -> (f r * M)%R @[r --> +oo] --> +oo.
+Lemma gt0_cvgMly {R : realFieldType} {F : set_system R} {FF : Filter F} (M : R)
+  (f : R -> R) :
+  (0 < M)%R -> f r @[r --> F] --> +oo -> (f r * M)%R @[r --> F] --> +oo.
 Proof.
 move=> M0 /cvgryPge fy; apply/cvgryPge => A.
-apply: filterS (fy (A / M)) => x.
-by rewrite ler_pdivrMr.
+by apply: filterS (fy (A / M)) => x; rewrite ler_pdivrMr.
 Qed.
 
 Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)