diff --git a/theories/realfun.v b/theories/realfun.v
index 1a910c5bb..6e2b0aa12 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -11,6 +11,11 @@ From HB Require Import structures.
 (* This file provides properties of standard real-valued functions over real  *)
 (* numbers (e.g., the continuity of the inverse of a continuous function).    *)
 (*                                                                            *)
+(*     nondecreasing_fun f == the function f is non-decreasing                *)
+(*     nonincreasing_fun f == the function f is non-increasing                *)
+(*        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       *)
 (*                                                                            *)
diff --git a/theories/sequences.v b/theories/sequences.v
index 394c9486c..5284356db 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -11,6 +11,11 @@ Require Import reals ereal signed topology normedtype landau.
 (* The purpose of this file is to gather generic definitions and lemmas about *)
 (* sequences.                                                                 *)
 (*                                                                            *)
+(*     nondecreasing_seq u == the sequence u is non-decreasing                *)
+(*     nonincreasing_seq u == the sequence u is non-increasing                *)
+(*        increasing_seq u == the sequence u is (strictly) increasing         *)
+(*        decreasing_seq u == the sequence u is (strictly) decreasing         *)
+(*                                                                            *)
 (* * About sequences of real numbers:                                         *)
 (*        [sequence u_n]_n == the sequence of general element u_n             *)
 (*                  R ^nat == notation for the type of sequences, i.e.,       *)