diff --git a/theories/derive.v b/theories/derive.v
index aadc6c86c9..d6e1ae9ffa 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -28,6 +28,10 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau.
 (*                         and R : numFieldType                               *)
 (*               f^`()  == the derivative of f of domain R                    *)
 (*               f^`(n) == the nth derivative of f of domain R                *)
+(*  is_derive x v f df  == the derivative of a function f at point x along v  *)
+(*                         is df and f is derivable at x along v              *)
+(*      is_diff x f df  == the differential of a function f at point x is df  *)
+(*                          and f is differentiable at point x                 *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* Naming convention in this file:                                            *)
@@ -40,6 +44,59 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau.
 (*   (e.g., `derive1_cst`, `derive1_comp`)                                    *)
 (* - lemmas of the form `... -> is_derive x v f df` are named `is_derive*`    *)
 (*   (e.g., `is_derive_cst`)                                                  *)
+(* - lemmas of the form `... -> is_diff x f df` are named `is_diff*`          *)
+(*   (e.g., `is_diff_cst`)                                                    *)
+(*                                                                            *)
+(* # Automatic derivation and differentiation with `is_diff _` and            *)
+(*  `is_derive _`                                                             *)
+(*                                                                            *)
+(* Statements of the form `is_diff _` and `is_derive _` are typeclasses       *)
+(* registered via `Instance` declarations with a proof `ex_derive`/`ex_diff   *)
+(* of derivability/differentiability of the expression and a proof            *)
+(* `derive_val`/`diff_val` of the value of the derivative/differential        *)
+(* of the function ; so that typeclass resolution can automatically synthesize*)
+(* the differential/derivative of a compound expression from the              *)
+(* differentials/derivatives of its parts, instead of requiring the user to   *)
+(* prove and compute derivatives by hand.                                     *)
+(*                                                                            *)
+(* ## Lemmas of the form `is_derive _` and `is_diff _`                        *)
+(*                                                                            *)
+(* For a compound expression, e.g. built from f and g, state the goal with the*)
+(* expected derivative/differential and let typeclass resolution fill the     *)
+(* proof by `apply: is_derive_eq / is_diff_eq.` :                             *)
+(*  `Lemma is_derive_example (W : normedModType R)                            *)
+(*    (t : R^o) (f g : R^o -> W) (f' g' : W) v :                              *)
+(*    is_derive t v f f' ->                                                   *)
+(*    is_derive t v g g' ->                                                   *)
+(*    is_derive t v (f + g) (f'+g').                                          *)
+(* Proof. move => is_der_f is_der_g. by apply: is_derive_eq. Qed.`            *)
+(*                                                                            *)
+(* The proof is inferred structurally by chaining declared `is_derive _` or   *)
+(* `is_diff _` instances matching the pattern of the goal stated.             *)
+(*                                                                            *)
+(* To verify if a given expression is derivable or differentiable, you can use*)
+(* `apply: ex_derive. or `apply: ex_diff`, given the right                    *)
+(* `is_derive _` or `is_diff _` instances are defined such as :               *)
+(* Hypothesis derivable_f : forall t, derivable f t 1.                        *)
+(* Hypothesis derivable_h : forall t, derivable h t 1.                        *)
+(* Local Instance is_derive_f t : is_derive t 1 f ('D_1 f t).                 *)
+(* by apply: derivableP. Qed.                                                 *)
+(* Local Instance is_derive_h t : is_derive t 1 h ('D_1 h t).                 *)
+(* by apply: derivableP. Qed.                                                 *)
+(*                                                                            *)
+(* Lemma is_derivable_example (t : R^o) : derivable (f+h) t 1.                *)
+(* Proof. apply/ex_derive. Qed.                                               *)
+(*                                                                            *)
+(* To verify the value of a given function you can apply `derive_val` or      *)
+(* diff_val`, given the right `is_derive/diff` instances are defined such as :*)
+(*                                                                            *)
+(* Lemma is_derive_val_example t :                                            *)
+(* 'D_1 (f + h) t = ('D_1 f t) + ('D_1 h t). Proof. by apply/derive_val. Qed. *)
+(*                                                                            *)
+(* It is worth mentioning that every differentiable function is derivable     *)
+(* via the lemma `diff_derivable` and that a function is differentiable iff   *)
+(* it is derivable in the case of functions from R to a normed module,        *)
+(* via the lemma `derivable1_diffP`.                                          *)
 (*                                                                            *)
 (******************************************************************************)