diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 771d259a9f..2e6c35ed69 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -133,6 +133,8 @@
 - moved from `lebesgue_measure.v` to `set_interval.v`: `is_open_itv`, and
     `open_itv_cover`
 
+- moved `summability.v` from `theories` to `theories/showcase`
+
 ### Renamed
 
 - in `lebesgue_measure.v`:
diff --git a/_CoqProject b/_CoqProject
index 54e246e2da..b8ce0b1f59 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -46,13 +46,13 @@ theories/lebesgue_integral.v
 theories/ftc.v
 theories/hoelder.v
 theories/probability.v
-theories/summability.v
 theories/signed.v
 theories/itv.v
 theories/convex.v
 theories/charge.v
 theories/kernel.v
 theories/showcase/uniform_bigO.v
+theories/showcase/summability.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v
diff --git a/theories/Make b/theories/Make
index f4e9346fc8..9dfe5bd5fe 100644
--- a/theories/Make
+++ b/theories/Make
@@ -34,7 +34,6 @@ ftc.v
 hoelder.v
 probability.v
 lebesgue_stieltjes_measure.v
-summability.v
 signed.v
 itv.v
 convex.v
@@ -42,6 +41,7 @@ charge.v
 kernel.v
 all_analysis.v
 showcase/uniform_bigO.v
+showcase/summability.v
 altreals/xfinmap.v
 altreals/discrete.v
 altreals/realseq.v
diff --git a/theories/all_analysis.v b/theories/all_analysis.v
index a2e395fb38..6a3e1bc010 100644
--- a/theories/all_analysis.v
+++ b/theories/all_analysis.v
@@ -25,7 +25,6 @@ From mathcomp Require Export ftc.
 From mathcomp Require Export hoelder.
 From mathcomp Require Export probability.
 From mathcomp Require Export lebesgue_stieltjes_measure.
-From mathcomp Require Export summability.
 From mathcomp Require Export signed.
 From mathcomp Require Export itv.
 From mathcomp Require Export convex.
diff --git a/theories/realfun.v b/theories/realfun.v
index 1562ef5ff2..bf7048b22d 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -20,8 +20,9 @@ From HB Require Import structures.
 (*         increasing_fun f == the function f is (strictly) increasing        *)
 (*         decreasing_fun f == the function f is (strictly) decreasing        *)
 (*                                                                            *)
-(*   derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and       *)
-(*                             continuous up to the boundary                  *)
+(*   derivable_oo_continuous_bnd f x y == f is derivable in `]x, y[ and       *)
+(*                             continuous up to the boundary, i.e.,           *)
+(*                             f @ x^'+ --> f x  and  f @ y^'- --> f y        *)
 (*                                                                            *)
 (*      itv_partition a b s == s is a partition of the interval `[a, b]       *)
 (*       itv_partitionL s c == the left side of splitting a partition at c    *)
diff --git a/theories/summability.v b/theories/showcase/summability.v
similarity index 87%
rename from theories/summability.v
rename to theories/showcase/summability.v
index 09915bb100..b2679d0274 100644
--- a/theories/summability.v
+++ b/theories/showcase/summability.v
@@ -7,7 +7,8 @@ From mathcomp Require Import boolp classical_sets.
 Require Import ereal reals Rstruct signed topology normedtype.
 
 (**md**************************************************************************)
-(* (undocumented experiment)                                                  *)
+(* This file proposes a replacement for the definition `summable` (file       *)
+(* `realsum.v`).                                                              *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -17,16 +18,14 @@ Import GRing.Theory Num.Def Num.Theory.
 
 Local Open Scope classical_set_scope.
 
-(** For Pierre-Yves : definition of sums *)
-
 From mathcomp Require fintype bigop finmap.
 
 Section totally.
 
 Import fintype bigop finmap.
 Local Open Scope fset_scope.
-(* :TODO: when eventually is generalized to any lattice *)
-(* totally can just be replaced by eventually *)
+(* TODO: when eventually is generalized to any lattice, totally can
+   just be replaced by eventually *)
 Definition totally {I : choiceType} : set_system {fset I} :=
   filter_from setT (fun A => [set B | A `<=` B]).
 
diff --git a/theories/showcase/uniform_bigO.v b/theories/showcase/uniform_bigO.v
index 1eb7e8bf72..dfb9d6a29e 100644
--- a/theories/showcase/uniform_bigO.v
+++ b/theories/showcase/uniform_bigO.v
@@ -14,18 +14,13 @@ Local Open Scope ring_scope.
 
 Section UniformBigO.
 
-(*
-  This section shows how we can formalize the uniform bigO from:
-
-  Boldo, Clément, Filliâtre, Mayero, Melquiond, Weis.
-  Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C
-  Program.
-  Journal of Automated Reasoning 2013.
-
-  The corresponding source code is here:
-
-  http://fost.saclay.inria.fr/coq_total/BigO.html
-*)
+(**md**************************************************************************)
+(* This section shows how we can formalize the uniform bigO from:             *)
+(* Boldo, Clément, Filliâtre, Mayero, Melquiond, Weis,                        *)
+(* Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a  *)
+(* C Program, Journal of Automated Reasoning 2013. The corresponding source   *)
+(* code is here: http://fost.saclay.inria.fr/coq_total/BigO.html.             *)
+(******************************************************************************)
 
 Context (A : Type) (P : set (R * R)).