diff --git a/coq/ch3.v b/coq/ch3.v
index 801d9782..d79cdb91 100644
--- a/coq/ch3.v
+++ b/coq/ch3.v
@@ -18,14 +18,82 @@ Check Prop.
 
 Lemma stamps n : 12 <= n -> exists s4 s5, s4 * 4 + s5 * 5 = n.
 Proof.
-elim: n {-2}n (leqnn n) =>[|n IHn]; first by case.
-do 12! [ case=> // ].
-case; first by exists 3, 0.
-case; first by exists 2, 1.
-case; first by exists 1, 2.
-case; first by exists 0, 3.
-move=> m'; set m := _.+1; move=> mn m11.
-case: (IHn (m-4) _ isT) => [|s4 [s5 def_m4]].
-  by rewrite leq_subLR (leq_trans mn) // addSnnS leq_addl.
+have [m leq_mn] := ubnPgeq n; elim: n => // n IHn in m leq_mn *; first by case: n => [|n] in IHn *.
+do 12! [ case: m => //= m in leq_mn * ] => _.
+case: m => [|m] in leq_mn *; first by exists 3, 0.
+case: m => [|m] in leq_mn *; first by exists 2, 1.
+case: m => [|m] in leq_mn *; first by exists 1, 2.
+case: m => [|m] in leq_mn *; first by exists 0, 3.
+case: (IHn ((16+m) - 4) _ isT) => [|s4 [s5 def_m4]]. 
+  by rewrite leq_subLR (leq_trans leq_mn) // addSnnS leq_addl.
 by exists s4.+1, s5; rewrite mulSn -addnA def_m4 subnKC.
 Qed.
+
+
+Fixpoint nat_ind (P : nat -> Prop)
+  (p0 : P 0) (pS : forall n : nat, P n -> P n.+1) n : P n :=
+  if n is m.+1 then
+    let pm (* : P m *) := nat_ind P p0 pS m in
+    pS m pm (* : P m.+1 *)
+  else p0.
+
+Lemma absurd : false = true -> forall P, P.
+Proof. by []. Qed. (* see coqart? *)
+
+Definition leq_trans n m o (Hmn : m <= n) (Hno : n <= o) : m <= o :=
+  nat_ind (fun n => forall m o, m <= n -> n <= o -> m <= o)
+    (fun m => match m with
+      | 0 => fun o Hmn Hno => (isT : 0 <= o)
+      | pm.+1 => fun o (Hmn : pm.+1 <= 0) Hno => absurd Hmn (pm.+1 <= o)
+      end)
+    (fun pn (IHn : forall m o : nat, m <= pn -> pn <= o -> m <= o) =>
+      fun m => match m with
+       | 0 => fun o Hmn Hno => (isT : 0 <= o)
+       | pm.+1 => fun o (Hmn : pm.+1 <= pn.+1) => match o with
+                   | 0 => fun (Hno : pn.+1 <= 0) => absurd Hno (pm.+1 <= 0)
+                   | po.+1 => fun (Hno : pn.+1 <= po.+1) =>
+                       IHn pm po (Hmn : pm <= pn) (Hno : pn <= po)
+                   end
+       end)
+    n
+  m o Hmn Hno.
+
+Definition strong_nat_ind (P : nat -> Prop)
+  (base : P 0)
+  (step : forall n, (forall m, m <= n -> P m) -> P n.+1) n : P n
+:=
+  nat_ind (fun n => forall m, m <= n -> P m)
+    (fun m => match m with
+      | 0 => fun Hmn => base
+      | pm.+1 => fun (Hmn : pm.+1 <= 0) => absurd Hmn (P pm.+1)
+      end)
+    (fun pn (IHn : forall m, m <= pn -> P m) =>
+      fun m => match m with
+       | 0 => fun Hmn => base
+       | pm.+1 => fun (Hmn : pm.+1 <= pn.+1) =>
+            let P_upto_pm j (Hjm : j <= pm) : P j :=
+              IHn j (leq_trans pm j pn Hjm (Hmn : pm <= pn)) in
+            step pm P_upto_pm
+       end)
+    n
+  n (leqnn n : n <= n).
+
+Axiom P : nat -> Prop.
+Check (nat_ind (fun n => forall m, m <= n -> P m)).
+(*
+: (forall m : nat, m <= 0 -> P m) ->
+(forall n : nat,
+ (forall m : nat, m <= n -> P m) -> forall m : nat, m <= n.+1 -> P m) ->
+forall n m : nat, m <= n -> P m
+*)
+Lemma  strong_nat_ind2 (P : nat -> Prop)
+  (base : P 0)
+  (step : forall n, (forall m, m <= n -> P m) -> P n.+1) x : P x.
+Proof.
+apply: (nat_ind (fun n => forall m, m <= n -> P m) _ _ x x (leqnn x)).
+  Show.
+  by case=> [_| //]; exact: base.
+move=> n IHn; case=> [_|m Hm]; first by exact: base.
+apply: step=> j Hjm; apply: IHn.
+apply: leq_trans Hjm Hm.
+Qed.
\ No newline at end of file
diff --git a/coq/ch4.v b/coq/ch4.v
index 6464fce5..d2c38bb2 100644
--- a/coq/ch4.v
+++ b/coq/ch4.v
@@ -72,17 +72,21 @@ Lemma edivn_recE d m q :
     if m - d is m'.+1 then edivn_rec d m' q.+1 else (q, m).
 Proof. by elim: m. Qed.
 
+Lemma test (G : nat -> Prop) m : G m.
+Proof.
+case: (ubnPgeq m). Show.
+
 Lemma edivnP m d (ed := edivn m d) :
   ((d > 0) ==> (ed.2 < d)) && (m == ed.1 * d + ed.2).
 Proof.
-case: d => [|d /=] in ed *; first by rewrite eqxx.
+rewrite -[m]/(0 * d + m).
+case: d => [//= | d /=] in ed *.
 rewrite -[edivn m d.+1]/(edivn_rec d m 0) in ed *.
-rewrite -[m]/(0 * d.+1 + m).
-elim: m {-2}m 0 (leqnn m) @ed => [[]//=|n IHn [//=|m]] q le_mn.
-rewrite edivn_recE subn_if_gt; case: ifP => [le_dm|lt_md]; last first.
+case: (ubnPgeq m) @ed; elim: m 0 => [|m IHm] q [/=|n] leq_nm //.
+rewrite edivn_recE subn_if_gt; case: ifP => [le_dm ed|lt_md]; last first.
   by rewrite /= ltnS ltnNge lt_md eqxx.
-have /(IHn _ q.+1) : m - d <= n by rewrite (leq_trans (leq_subr d m)).
-by rewrite /= mulSnr -addnA -subSS subnKC.
+rewrite -ltnS in le_dm; rewrite -(subnKC le_dm) addnA -mulSnr.
+by apply: IHm q.+1 (n-d) _; apply: leq_trans (leq_subr d n) leq_nm.
 Qed.
 
 Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
diff --git a/tex/chProofLanguage.tex b/tex/chProofLanguage.tex
index 759f4243..2378c8e1 100644
--- a/tex/chProofLanguage.tex
+++ b/tex/chProofLanguage.tex
@@ -542,256 +542,272 @@ \subsection{Pushing to the stack}
 %under the name \C{leq77}.
 
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Example: strengthening induction}
-\index[concept]{induction!strong}
-\index[concept]{induction!curse of values}
-\label{sec:strongind}
-
-As an exercise we show how the \C{elim} tactic combined with the bookkeeping
-operator ``\C{:}'' lets one perform, on the fly, a stronger variant of
-induction called ``course of values'' or ``strong induction''.
-% [DG] I've never seen it called "course of values". Apparently this
-% name is mostly used in computability theory? But "strong induction"
-% appears very often.
-%assia : TODO
-
-Claim: every amount of postage that is at least 12 cents
-can be made from 4-cent and 5-cent stamps.  The proof in the inductive
-step goes as follows.  There are obvious solutions for a postage between
-12 and 15 cents, so we can assume it is at least 16 cents.  Since
-the postage amount is at least 16, by using a 4-cents stamp we are back
-at a postage amount that, by induction, can be obtained as claimed.\hfill$\square$
-
-The tricky step is that we want to apply the induction hypothesis not
-on $n-1$, as usual, but on $n-4$, since we know how to turn a
-solution for a stamping amount problem $n$ to one for a problem of
-size $n+4$ (by using a 4-cent stamp).
-The induction hypothesis provided by \C{nat_ind}
-is not strong enough.  However we can use the \C{:} operator
-to \emph{load the goal} before performing the induction.
-%\footnote{See further below for explanations.}
-\index[ssr]{\C{set name := term}}
-
-\begin{coq}{}{}
-Lemma stamps n : 12 <= n -> exists s4 s5, s4 * 4 + s5 * 5 = n.
-Proof.
-elim: n {-2}n (leqnn n) =>[|n IHn]; first by case.
-\end{coq}
-
-Let's dissect this line 3. First of all,
-``\C{elim: n \{-2\}n (leqnn n).}'' is shorthand for
-``\C{move: (leqnn n). move: \{-2\}n. move: n. elim.}'' (the terms after the
-colon \C{:} are pushed to the stack, from right to left; and the
-\C{elim} tactic is applied afterwards to the top of the stack, which
-of course is the last term pushed to the stack). Let us see how these
-four steps transform the goal. At the beginning, the context and the
-goal are
-
-\begin{coqout}{}{width=11cm}
-  n : nat
-  ============================
-  11 < n -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n
-\end{coqout}
-
-The first of our
-four steps (``\C{move: (leqnn n)}'') pushes the additional
-assumption \C{n <= n} onto the stack (since \C{(leqnn n)} provides
-its proof); we are thus left with
-
-\begin{coqout}{}{width=11cm}
-  n : nat
-  ============================
-  n <= n -> 11 < n -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n
-\end{coqout}
-
-The second step (``\C{move: \{-2\}n}'') is more interesting. Recall
-that \C{move:} usually ``generalizes'' a variable (i.e., takes a
-variable appearing in the context, and binds it by the universal
-quantifier, so that the goal becomes a for-all statement). The prefix
-\C{\{-2\}} means ``all except for the 2nd occurrence in the goal''; so
-the idea is
-to generalize ``all except for the 2nd occurrence of $n$''. Of course,
-this implies that $n$ still has to remain in the context (unlike for
-``\C{move: n}''), so the
-bound variable of the universal quantifier has to be a fresh
-variable, picked automatically by \Coq{}. For example, \Coq{} might
-pick \C{n0} for its name, and so the state after the second step will
-be:
-
-\begin{coqout}{}{width=11cm}
-  n : nat
-  ============================
-  forall n0 : nat,
-  n0 <= n -> 11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
-\end{coqout}
-
-Notice how the \C{n} in ``\C{n0 <= n}'' has remained un-generalized,
-since it was the 2nd occurrence of $n$ before the second step.
-
-The third step (``\C{move: n}'') merely moves the \C{n} from the
-context to the goal. Thus, after the three ``\C{move}'' steps, we are
-left with proving the following claim:
-
-\begin{coqout}{}{}
-forall n n0 : nat,
-  n0 <= n -> 11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
-\end{coqout}
-
-The \C{elim} now applies induction on the top of the stack, which
-is \C{n}. The corresponding induction hypothesis \C{IHn} is:
-
-\begin{coqout}{}{}
-IHn : forall n0 : nat,
-      n0 <= n ->
-      11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
-\end{coqout}
-
-Of course, the \C{n} here is not the original \C{n}, but the new
-\C{n} introduced in the \C{=>[|n IHn]} pattern.
-
-The proof continues like that:
-
-\lstset{firstnumber=4}
-\begin{coq}{}{}
-do 12! [ case; first by [] ]. (* < 12c *)
-case; first by exists 3, 0.   (* 12c = 3 * 4c *)
-case; first by exists 2, 1.   (* 13c = 2 * 4c + 1 * 5c *)
-case; first by exists 1, 2.   (* 14c = 1 * 4c + 2 * 5c *)
-case; first by exists 0, 3.   (* 15c = 3 * 5c *)
-move=> m'; set m := _.+1; move=> mn m11.
-\end{coq}
-\lstset{firstnumber=1}
-
-Line 4 repeats a tactic 12 times using the \C{do 12!} tactical.
-This deals with the 12 cases where \C{n0} is not greater than 11.
-\index[ssr]{\C{do n"!} (iteration)}
-
-Lines from 5 to 8 provide solutions for 12, 13, 14 and 15 cents.
-At line 9, just after the \C{move=> m'} step, the goal is the following one:
-
-\begin{coqout}{}{}
-1 subgoal
-  
-  n : nat
-  IHn : forall n0 : nat, n0 <= n -> 
-	  11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
-  m' : nat
-  ============================
-  m'.+3.+4.+4.+4 < n.+1 ->
-    11 < m'.+4.+4.+4.+4 ->
-      exists s4 s5 : nat, s4 * 4 + s5 * 5 = m'.+4.+4.+4.+4
-\end{coqout}
-
-This goal is hard to read because of the many \C{.+1} piling
-up. \mcbMC{} has the notations \C{.+1},
-\C{.+2}, \C{.+3} and \C{.+4} pre-defined, but not \C{.+5} and higher,
-hence what could be in principle displayed as \C{.+15} is actually
-displayed as \C{.+3.+4.+4.+4}.
-
-We resort to the \C{set m := _.+1} tactic to build an abbreviation
-named \C{m} for the terms that match the pattern \C{_.+1}. As for the
-\C{rewrite} tactic, the goals is traversed from left to right, outside
-in, in order to find a term that matches the pattern.
-
-The first term encountered is \C{m'.+3.+4.+4.+4.+1}. Recall that
-the \C{<} infix notation hides an \C{.+1} on the left. Once
-the term above is extracted from its context the notation
-for \C{<} does not apply anymore: the abbreviation 
-displays as \C{(m := m'.+4.+4.+4.+4 : nat)} in the context,
-and the top assumption as \C{m <= n.+1}.
-
-After naming \C{mn} and \C{m11} the goal is the following one"
-
-\begin{coqout}{}{}
-  n : nat
-  IHn : forall n0 : nat, n0 <= n ->
-          11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
-  m' : nat
-  m := m'.+4.+4.+4.+4 : nat
-  mn : m <= n.+1
-  m11 : 11 < m
-  ============================
-  exists s4 s5 : nat, s4 * 4 + s5 * 5 = m
-\end{coqout}
-
+% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \subsection{Example: strengthening induction}
+% \index[concept]{induction!strong}
+% \index[concept]{induction!curse of values}
+% \label{sec:strongind}
 % 
-% Line 9 uses the \C{set} proof command to define a new
-% constant in the context. For example, ``\C{set a := 24 * 11.}'' would
-% create a new ``\C{a := 24 * 11 : nat}'' item in the context. The
-% command also tries to substitute the newly-defined constant for its
-% appearances in the goal; for example, ``\C{set a := 11.}'' would not
-% only create a new ``\C{a := 11 : nat}'' in the context, but also
-% replace the ``\C{11 < m'.+4.+4.+4.+4}'' in the goal\footnote{Don't be
-% surprised by the fact that an addition of 16 is circumscribed by four
-% additions of 4. By default, \mcbMC{} has the notations \C{.+1},
-% \C{.+2}, \C{.+3} and \C{.+4} pre-defined, but not \C{.+5} and higher.}
-% by an ``\C{a < m'.+4.+4.+4.+4}''. In our example above
-% (``\C{set m := _.+1}''), we are using the
-% \C{set} command with a wildcard; this captures the first term of the
-% form \C{_.+1} appearing in the goal and denotes it by \C{m}, replacing
-% it by \C{m} on the goal. In our case, this first term is
-% \C{m'.+4.+4.+4.+4} (which is just syntactic sugar for
-% \C{m'.+1.+1.....} with 16 appearances of \C{.+1})\footnote{This is
-% slightly counterintuitive, as you
-% might instead believe it to be \C{m'.+3.+4.+4.+4}. But keep in mind
-% that \C{m'.+3.+4.+4.+4 < n.+1} is just syntactic sugar for
-% \C{m'.+4.+4.+4.+4 <= n.+1}.},
-% % [DG] I hope I got these subtleties right. That said, I think it
-% % would be better to first introduce the "set" tactic in a less
-% % confusing example.
+% As an exercise we show how the \C{elim} tactic combined with the bookkeeping
+% operator ``\C{:}'' lets one perform, on the fly, a stronger variant of
+% induction called ``course of values'' or ``strong induction''.
+% % [DG] I've never seen it called "course of values". Apparently this
+% % name is mostly used in computability theory? But "strong induction"
+% % appears very often.
 % %assia : TODO
-% and so the name \C{m} is given to this term. We could have achieved
-% the same goal using ``\C{set m := m'.+4.+4.+4.+4}''.
-% \par
-% Further details about the \C{set} tactic can be found in
-% \cite[\S 4.2]{ssrman}; let us only mention the (by now) habitual
-% variant \C{set a := \{k\}(pattern)}, which defines a new constant
-% \C{a} to equal the first subterm of the goal that matches the pattern
-% \C{pattern}, but then replaces \emph{only the \(k\)-th} appearance
-% of this subterm in the goal by \C{a}. As usual, if the
-% pattern-matching algorithm keeps finding the wrong subterms, it is
-% always possible to completely specify the subterm, leaving no
-% wildcards.
-
-The proof continues as follows:
-
-\lstset{firstnumber=10}
-\begin{coq}{}{}
-case: (IHn (m-4) _ isT) => [|s4 [s5 def_m4]].
-  by rewrite leq_subLR (leq_trans mn) // addSnnS leq_addl.
-by exists s4.+1, s5; rewrite mulSn -addnA def_m4 subnKC.
-Qed.
-\end{coq}
-\lstset{firstnumber=1}
-
-Line 10 instantiates the induction hypothesis with the value
-\C{(m-4)}, with a placeholder for a missing proof of \C{(m-4 < n)},
-and with a proof that \C{(11 < m-4)}. The proof given for
-\C{(11 < m-4)} can be just \C{isT} since the type \C{(11 < m-4)} 
-\emph{computes} to \C{true} since the value of \C{m} is larger than 11.
-The missing proof
-of \C{(m-4 < n)}  becomes the first
-subgoal, solved at line 11.
-
-The induction hypothesis yields
-\C{exists s4 s5 : nat, s4 * 4 + s5 * 5 = m-4}. The introduction
-pattern in line 10 gives names to the values of \C{s4} and \C{s5}
-whose existence is thus guaranteed, and named \C{def_m4} the
-assumption
-\C{s4 * 4 + s5 * 5 = m-4}. In other words, it gives names \C{s4} and
-\C{s5} to the quantities of 4-cent and 5-cent stamps needed to cover
-the amount of postage \C{(m-4)}, as well as to the fact that they do
-cover this exact amount of postage. The intro pattern to name
-\C{s5} needs an extra destructing pattern (square bracket) because
-\C{(exists s4 s5, ...)} is just a notation for
-\C{(exists s4, exists s5, ...)} hence two existential
-quantifiers need to be actually dealt with.
-
-Line 12 gives the final solution: by using one extra 4 cents stamp
-we can appeal to the induction hypothesis.
-
-
+% 
+% Claim: every amount of postage that is at least 12 cents
+% can be made from 4-cent and 5-cent stamps.  The proof in the inductive
+% step goes as follows.  There are obvious solutions for a postage between
+% 12 and 15 cents, so we can assume it is at least 16 cents.  Since
+% the postage amount is at least 16, by using a 4-cents stamp we are back
+% at a postage amount that, by induction, can be obtained as claimed.\hfill$\square$
+% 
+% The tricky step is that we want to apply the induction hypothesis not
+% on $n-1$, as usual, but on $n-4$, since we know how to turn a
+% solution for a stamping amount problem $n$ to one for a problem of
+% size $n+4$ (by using a 4-cent stamp).
+% The induction hypothesis provided by \C{nat_ind}
+% is not strong enough.  However we can use the \C{:} operator
+% to \emph{load the goal} before performing the induction.
+% %\footnote{See further below for explanations.}
+% \index[ssr]{\C{set name := term}}
+% 
+% \begin{coq}{}{}
+% Lemma stamps n : 12 <= n -> exists s4 s5, s4 * 4 + s5 * 5 = n.
+% Proof.
+% have [m leq_mn] := ubnPgeq n; elim: n => // n IHn in m leq_mn *; first by case: n => [|n] in IHn *.
+% do 12! [ case: m => //= m in leq_mn * ] => _.
+% case: m => [|m] in leq_mn *; first by exists 3, 0.
+% case: m => [|m] in leq_mn *; first by exists 2, 1.
+% case: m => [|m] in leq_mn *; first by exists 1, 2.
+% case: m => [|m] in leq_mn *; first by exists 0, 3.
+% case: (IHn ((16+m) - 4) _ isT) => [|s4 [s5 def_m4]].
+%   by rewrite leq_subLR (leq_trans leq_mn) // addSnnS leq_addl.
+% by exists s4.+1, s5; rewrite mulSn -addnA def_m4 subnKC.
+% Qed.
+% \end{coq}
+% 
+% 
+% \begin{coq}{}{}
+% Lemma stamps n : 12 <= n -> exists s4 s5, s4 * 4 + s5 * 5 = n.
+% Proof.
+% elim: n {-2}n (leqnn n) =>[|n IHn]; first by case.
+% \end{coq}
+% 
+% Let's dissect this line 3. First of all,
+% ``\C{elim: n \{-2\}n (leqnn n).}'' is shorthand for
+% ``\C{move: (leqnn n). move: \{-2\}n. move: n. elim.}'' (the terms after the
+% colon \C{:} are pushed to the stack, from right to left; and the
+% \C{elim} tactic is applied afterwards to the top of the stack, which
+% of course is the last term pushed to the stack). Let us see how these
+% four steps transform the goal. At the beginning, the context and the
+% goal are
+% 
+% \begin{coqout}{}{width=11cm}
+%   n : nat
+%   ============================
+%   11 < n -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n
+% \end{coqout}
+% 
+% The first of our
+% four steps (``\C{move: (leqnn n)}'') pushes the additional
+% assumption \C{n <= n} onto the stack (since \C{(leqnn n)} provides
+% its proof); we are thus left with
+% 
+% \begin{coqout}{}{width=11cm}
+%   n : nat
+%   ============================
+%   n <= n -> 11 < n -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n
+% \end{coqout}
+% 
+% The second step (``\C{move: \{-2\}n}'') is more interesting. Recall
+% that \C{move:} usually ``generalizes'' a variable (i.e., takes a
+% variable appearing in the context, and binds it by the universal
+% quantifier, so that the goal becomes a for-all statement). The prefix
+% \C{\{-2\}} means ``all except for the 2nd occurrence in the goal''; so
+% the idea is
+% to generalize ``all except for the 2nd occurrence of $n$''. Of course,
+% this implies that $n$ still has to remain in the context (unlike for
+% ``\C{move: n}''), so the
+% bound variable of the universal quantifier has to be a fresh
+% variable, picked automatically by \Coq{}. For example, \Coq{} might
+% pick \C{n0} for its name, and so the state after the second step will
+% be:
+% 
+% \begin{coqout}{}{width=11cm}
+%   n : nat
+%   ============================
+%   forall n0 : nat,
+%   n0 <= n -> 11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
+% \end{coqout}
+% 
+% Notice how the \C{n} in ``\C{n0 <= n}'' has remained un-generalized,
+% since it was the 2nd occurrence of $n$ before the second step.
+% 
+% The third step (``\C{move: n}'') merely moves the \C{n} from the
+% context to the goal. Thus, after the three ``\C{move}'' steps, we are
+% left with proving the following claim:
+% 
+% \begin{coqout}{}{}
+% forall n n0 : nat,
+%   n0 <= n -> 11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
+% \end{coqout}
+% 
+% The \C{elim} now applies induction on the top of the stack, which
+% is \C{n}. The corresponding induction hypothesis \C{IHn} is:
+% 
+% \begin{coqout}{}{}
+% IHn : forall n0 : nat,
+%       n0 <= n ->
+%       11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
+% \end{coqout}
+% 
+% Of course, the \C{n} here is not the original \C{n}, but the new
+% \C{n} introduced in the \C{=>[|n IHn]} pattern.
+% 
+% The proof continues like that:
+% 
+% \lstset{firstnumber=4}
+% \begin{coq}{}{}
+% do 12! [ case; first by [] ]. (* < 12c *)
+% case; first by exists 3, 0.   (* 12c = 3 * 4c *)
+% case; first by exists 2, 1.   (* 13c = 2 * 4c + 1 * 5c *)
+% case; first by exists 1, 2.   (* 14c = 1 * 4c + 2 * 5c *)
+% case; first by exists 0, 3.   (* 15c = 3 * 5c *)
+% move=> m'; set m := _.+1; move=> mn m11.
+% \end{coq}
+% \lstset{firstnumber=1}
+% 
+% Line 4 repeats a tactic 12 times using the \C{do 12!} tactical.
+% This deals with the 12 cases where \C{n0} is not greater than 11.
+% \index[ssr]{\C{do n"!} (iteration)}
+% 
+% Lines from 5 to 8 provide solutions for 12, 13, 14 and 15 cents.
+% At line 9, just after the \C{move=> m'} step, the goal is the following one:
+% 
+% \begin{coqout}{}{}
+% 1 subgoal
+%   
+%   n : nat
+%   IHn : forall n0 : nat, n0 <= n -> 
+% 	  11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
+%   m' : nat
+%   ============================
+%   m'.+3.+4.+4.+4 < n.+1 ->
+%     11 < m'.+4.+4.+4.+4 ->
+%       exists s4 s5 : nat, s4 * 4 + s5 * 5 = m'.+4.+4.+4.+4
+% \end{coqout}
+% 
+% This goal is hard to read because of the many \C{.+1} piling
+% up. \mcbMC{} has the notations \C{.+1},
+% \C{.+2}, \C{.+3} and \C{.+4} pre-defined, but not \C{.+5} and higher,
+% hence what could be in principle displayed as \C{.+15} is actually
+% displayed as \C{.+3.+4.+4.+4}.
+% 
+% We resort to the \C{set m := _.+1} tactic to build an abbreviation
+% named \C{m} for the terms that match the pattern \C{_.+1}. As for the
+% \C{rewrite} tactic, the goals is traversed from left to right, outside
+% in, in order to find a term that matches the pattern.
+% 
+% The first term encountered is \C{m'.+3.+4.+4.+4.+1}. Recall that
+% the \C{<} infix notation hides an \C{.+1} on the left. Once
+% the term above is extracted from its context the notation
+% for \C{<} does not apply anymore: the abbreviation 
+% displays as \C{(m := m'.+4.+4.+4.+4 : nat)} in the context,
+% and the top assumption as \C{m <= n.+1}.
+% 
+% After naming \C{mn} and \C{m11} the goal is the following one"
+% 
+% \begin{coqout}{}{}
+%   n : nat
+%   IHn : forall n0 : nat, n0 <= n ->
+%           11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
+%   m' : nat
+%   m := m'.+4.+4.+4.+4 : nat
+%   mn : m <= n.+1
+%   m11 : 11 < m
+%   ============================
+%   exists s4 s5 : nat, s4 * 4 + s5 * 5 = m
+% \end{coqout}
+% 
+% % 
+% % Line 9 uses the \C{set} proof command to define a new
+% % constant in the context. For example, ``\C{set a := 24 * 11.}'' would
+% % create a new ``\C{a := 24 * 11 : nat}'' item in the context. The
+% % command also tries to substitute the newly-defined constant for its
+% % appearances in the goal; for example, ``\C{set a := 11.}'' would not
+% % only create a new ``\C{a := 11 : nat}'' in the context, but also
+% % replace the ``\C{11 < m'.+4.+4.+4.+4}'' in the goal\footnote{Don't be
+% % surprised by the fact that an addition of 16 is circumscribed by four
+% % additions of 4. By default, \mcbMC{} has the notations \C{.+1},
+% % \C{.+2}, \C{.+3} and \C{.+4} pre-defined, but not \C{.+5} and higher.}
+% % by an ``\C{a < m'.+4.+4.+4.+4}''. In our example above
+% % (``\C{set m := _.+1}''), we are using the
+% % \C{set} command with a wildcard; this captures the first term of the
+% % form \C{_.+1} appearing in the goal and denotes it by \C{m}, replacing
+% % it by \C{m} on the goal. In our case, this first term is
+% % \C{m'.+4.+4.+4.+4} (which is just syntactic sugar for
+% % \C{m'.+1.+1.....} with 16 appearances of \C{.+1})\footnote{This is
+% % slightly counterintuitive, as you
+% % might instead believe it to be \C{m'.+3.+4.+4.+4}. But keep in mind
+% % that \C{m'.+3.+4.+4.+4 < n.+1} is just syntactic sugar for
+% % \C{m'.+4.+4.+4.+4 <= n.+1}.},
+% % % [DG] I hope I got these subtleties right. That said, I think it
+% % % would be better to first introduce the "set" tactic in a less
+% % % confusing example.
+% % %assia : TODO
+% % and so the name \C{m} is given to this term. We could have achieved
+% % the same goal using ``\C{set m := m'.+4.+4.+4.+4}''.
+% % \par
+% % Further details about the \C{set} tactic can be found in
+% % \cite[\S 4.2]{ssrman}; let us only mention the (by now) habitual
+% % variant \C{set a := \{k\}(pattern)}, which defines a new constant
+% % \C{a} to equal the first subterm of the goal that matches the pattern
+% % \C{pattern}, but then replaces \emph{only the \(k\)-th} appearance
+% % of this subterm in the goal by \C{a}. As usual, if the
+% % pattern-matching algorithm keeps finding the wrong subterms, it is
+% % always possible to completely specify the subterm, leaving no
+% % wildcards.
+% 
+% The proof continues as follows:
+% 
+% \lstset{firstnumber=10}
+% \begin{coq}{}{}
+% case: (IHn (m-4) _ isT) => [|s4 [s5 def_m4]].
+%   by rewrite leq_subLR (leq_trans mn) // addSnnS leq_addl.
+% by exists s4.+1, s5; rewrite mulSn -addnA def_m4 subnKC.
+% Qed.
+% \end{coq}
+% \lstset{firstnumber=1}
+% 
+% Line 10 instantiates the induction hypothesis with the value
+% \C{(m-4)}, with a placeholder for a missing proof of \C{(m-4 < n)},
+% and with a proof that \C{(11 < m-4)}. The proof given for
+% \C{(11 < m-4)} can be just \C{isT} since the type \C{(11 < m-4)} 
+% \emph{computes} to \C{true} since the value of \C{m} is larger than 11.
+% The missing proof
+% of \C{(m-4 < n)}  becomes the first
+% subgoal, solved at line 11.
+% 
+% The induction hypothesis yields
+% \C{exists s4 s5 : nat, s4 * 4 + s5 * 5 = m-4}. The introduction
+% pattern in line 10 gives names to the values of \C{s4} and \C{s5}
+% whose existence is thus guaranteed, and named \C{def_m4} the
+% assumption
+% \C{s4 * 4 + s5 * 5 = m-4}. In other words, it gives names \C{s4} and
+% \C{s5} to the quantities of 4-cent and 5-cent stamps needed to cover
+% the amount of postage \C{(m-4)}, as well as to the fact that they do
+% cover this exact amount of postage. The intro pattern to name
+% \C{s5} needs an extra destructing pattern (square bracket) because
+% \C{(exists s4 s5, ...)} is just a notation for
+% \C{(exists s4, exists s5, ...)} hence two existential
+% quantifiers need to be actually dealt with.
+% 
+% Line 12 gives the final solution: by using one extra 4 cents stamp
+% we can appeal to the induction hypothesis.
+% 
+% 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Structuring proofs, by examples}
 
diff --git a/tex/chSpecification.tex b/tex/chSpecification.tex
index 99558962..e59279c9 100644
--- a/tex/chSpecification.tex
+++ b/tex/chSpecification.tex
@@ -993,6 +993,65 @@ \subsection{Inductive specs with indices}\label{ssec:specs}
 % \item Tuning of implicit arguments
 % \end{itemize}
 
+\section{Strong induction via inductive specs}
+\label{sec:ubnP}
+
+As we have seen in Section~\ref{ssec:indreason} the strong induction principle
+can be obtained from the regular one by choosing an appropriate value for
+the predicate. Recall that the \C{elim} tactic infers that predicate from the
+goal, so another way to specify the predicate is to \emph{load} the goal
+before performing the induction.
+For example if the goal is \C{(G n)} and one loads it to
+\C{(forall m, m <= n -> G m)} then he will have access to the
+induction hypothesis on all numbers smaller than \C{n} exactly as
+if he was using the strong induction principle.
+
+It is possible to
+do so very concisely using the discharging operator ``\C{:}''.
+In particular
+\begin{coq}{}{}
+move: {-2}n (leqnn n)
+\end{coq}{}{}
+does exactly what we need
+for a goal like \C{(G n)}: it first pushes to the stack \C{(n <= n)}
+and then pushes to the stack \C{n} capturing all occurrences but for
+the second one.
+The \mcbMC{} library provides a few tools to load the goal like this
+without recurring to occurrence selection, which can be tricky and fragile.
+
+The following inductive specification is crafted so that its only constructor
+holds as arguments exactly the items we pushed on the stack with the discharge
+operator.
+
+\begin{coq}{}{}
+Inductive ubn_geq_spec m : nat -> Type :=
+  UbnGeq n of n <= m : ubn_geq_spec m n.
+Lemma ubnPgeq m : ubn_geq_spec m m.
+Proof. by []. Qed.
+\end{coq}{}{}
+\index[coq]{\C{ubnPgeq}}
+
+As a consequence by performing a case analysis on \C{(ubnPgeq n)} one
+obtains the same effect of \C{move: {-2}n (leqnn n)}.
+
+\begin{coq}{}{}
+Lemma test_ubnP (G : nat -> Prop) n : G n.
+Proof.
+case: (ubnPgeq m).
+\end{coq}{}{}
+\begin{coqout}{}{}
+G : nat -> Prop
+n : nat
+============================
+forall m, m <= n -> G m
+\end{coqout}{}{}
+
+By varying the arguments of the inductive specification constructor one
+can tune the way the goal is loaded. The \mcbMC{} library
+provides a few inductive specifications like the one
+explained in this section, and their names contain the string
+``ubn'' for ``upper bound''.
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \clearpage
 \section{Showcase: Euclidean division, simple and correct}\label{sec:edivn}
@@ -1045,21 +1104,19 @@ \section{Showcase: Euclidean division, simple and correct}\label{sec:edivn}
 
 As one expects, \C{edivn} being a recursive program, its specification
 needs to be proved by induction.  Given that the recursive call is on
-the subtraction of the input, we need to perform a strong induction,
-as we did for the postage example in section~\ref{sec:strongind}.
+the subtraction of the input, we need to perform a strong induction.
 
 But let's start by dealing with the trivial case of a null divisor.
 
 \begin{coq}{}{}
-case: d => [//=|d /=] in ed *.
+rewrite -[m]/(0 * d + m).
+case: d => [//= | d /=] in ed *.
 rewrite -[edivn m d.+1]/(edivn_rec d m 0) in ed *.
-rewrite -[m]/(0 * d.+1 + m).
-elim: m {-2}m 0 (leqnn m) @ed => [[]//=|n IHn [//=|m]] q le_mn.
-rewrite edivn_recE subn_if_gt; case: ifP => [le_dm|lt_md]; last first.
+case: (ubnPgeq m) @ed; elim: m 0 => [|m IHm] q [/=|n] leq_nm //.
+rewrite edivn_recE subn_if_gt; case: ifP => [le_dm ed|lt_md]; last first.
   by rewrite /= ltnS ltnNge lt_md eqxx.
-have /(IHn _ q.+1) : m - d <= n by rewrite (leq_trans (leq_subr d m)).
-by rewrite /= mulSnr -addnA -subSS subnKC.
-Qed.
+rewrite -ltnS in le_dm; rewrite -(subnKC le_dm) addnA -mulSnr subSS.
+by apply: IHm q.+1 (n-d) _; apply: leq_trans (leq_subr d n) leq_nm.
 \end{coq}
 \index[ssr]{\C{tactic in name}}
 Line 1 handles the case of \C{d} being zero.  The ``\C{in E...}'' suffix
@@ -1079,23 +1136,27 @@ \section{Showcase: Euclidean division, simple and correct}\label{sec:edivn}
 value of the accumulator \C{0}, leading to the following goal:
 
 \begin{coqout}{}{}
-d, n : nat
-IHn : forall m n0 : nat, m <= n ->
-      let ed := edivn_rec d m n0 in
-        (ed.2 < d.+1) && (n0 * d.+1 + m == ed.1 * d.+1 + ed.2)
-m, q : nat
-le_mn : m < n.+1
-========================
-let ed := edivn_rec d m.+1 q in
-  (ed.2 < d.+1) && (q * d.+1 + m.+1 == ed.1 * d.+1 + ed.2)
+d, m : nat
+IHm : forall q n, n <= m ->
+  let ed := edivn_rec d n q in
+  (ed.2 < d.+1) && (q * d.+1 + n == ed.1 * d.+1 + ed.2)
+q, n : nat
+leq_nm : n < m.+1
+============================
+let ed := edivn_rec d n.+1 q in
+(ed.2 < d.+1) && (q * d.+1 + n.+1 == ed.1 * d.+1 + ed.2)
 \end{coqout}
-Note that the induction touches variables used in \C{ed} that
-is hence pushed on the goal stack.  The \C{@} modifier tells SSReflect
-to keep the body of the let-in.
+
+Note that the case analysis on \C{(ubnPgeq m)} needs to grab also
+the occurrence of \C{m} in the body of \C{ed}. To do so
+we push \C{ed} on the goal stack prior the case analysis.  The \C{@} modifier
+tells \mcbSSR{} to keep the body of the let-in, which would be otherwise
+deleted.
 
 Line 5 unfolds the recursive function and uses the following lemma to push the
 subtraction into the branches of the if statement. Then it reasons by cases
 on the guard of the if-then-else statement.
+
 %\marginnote{Should we embed this lemma in the unfolding equation?}
 
 \begin{coq}{}{}
@@ -1106,9 +1167,30 @@ \section{Showcase: Euclidean division, simple and correct}\label{sec:edivn}
 
 The else branch corresponds to the non-recursive case of
 the division algorithm and is trivially solved in line 6.
-The recursive call is done on \C{(m-d)}, hence the need for a strong
-induction.  In order to satisfy the premise of the induction hypothesis,
-line 7 shows that \C{(m - d <= n)}.  Line 8 concludes.
+We are left with this goal to prove:
+
+\begin{coqout}{}{}
+d, m : nat
+IHm : forall q n, n <= m ->
+  let ed := edivn_rec d n q in
+  (ed.2 < d.+1) && (q * d.+1 + n == ed.1 * d.+1 + ed.2)
+q, n : nat
+leq_nm : n < m.+1
+le_dm : d <= n
+ed := edivn_rec d (n - d) q.+1 : nat * nat
+============================
+(ed.2 < d.+1) && (q * d.+1 + n.+1 == ed.1 * d.+1 + ed.2)
+\end{coqout}
+
+Line 7 prepares the goal to accommodate the application of the induction
+hypothesis, instantiated at \C{q.+1} and \C{(n - d)}.
+
+\begin{coqout}{}{}
+(ed.2 < d.+1) && (q.+1 * d.+1 + (n - d) == ed.1 * d.+1 + ed.2)
+\end{coqout}
+
+Finally, line 8 uses the induction hypothesis and proves its premise
+\C{(m - d <= n)}.
 
 % \section{STOP HERE}
 %
diff --git a/tex/chTT.tex b/tex/chTT.tex
index 79c917f3..61edeec3 100644
--- a/tex/chTT.tex
+++ b/tex/chTT.tex
@@ -1125,7 +1125,58 @@ \section{Inductive reasoning}\label{ssec:indreason}
 
 The \Coq{} system generates this program automatically, as soon as
  the \C{nat} data type
-is defined.  Recall that recursive functions are checked for termination:
+is defined. 
+
+It is worth mentioning that this principle is general enough to
+prove the ``stronger'' induction principle that give access, in
+the inductive step, to the property \C{P} on all numbers
+small than \C{n.+1} and not just its predecessor.
+
+\begin{coq}{}{}
+Lemma strong_nat_ind (P : nat -> Prop)
+  (base : P 0)
+  (step : forall n, (forall m, m <= n -> P m) -> P n.+1) x : P x.
+\end{coq}{}{}
+
+In order to prove this statement it is sufficient to craft
+the right ``P'' for \c{nat_ind}.
+
+\begin{coq}{}{}
+Check (nat_ind (fun n => forall m, m <= n -> P m)).
+\end{coq}{}{}
+\begin{coqout}{}{}
+  (forall m, m <= 0 -> P m) ->
+  (forall n, (forall m, m <= n -> P m) -> forall m, m <= n.+1 -> P m) ->
+  forall n m, m <= n -> P m
+\end{coqout}{}{}
+
+If we fulfill the last premise with \C{(leqnn x : x <= x)} we obtain
+the following proof goals:
+
+\begin{coq}{}{}
+Proof.
+apply: (nat_ind (fun n => forall m, m <= n -> P m) _ _ x x (leqnn x)).
+\end{coq}{}{}
+\begin{coqout}{}{}
+  P : nat -> Prop
+  base : P 0
+  step : forall n : nat, (forall m : nat, m <= n -> P m) -> P n.+1
+  x : nat
+  ============================
+  forall m : nat, m <= 0 -> P m
+
+subgoal 2 is:
+ forall n : nat,
+ (forall m : nat, m <= n -> P m) -> forall m : nat, m <= n.+1 -> P m
+\end{coqout}{}{}
+
+The two goals follow from \C{base} and \C{step} respectively.
+Induction principles like this one can be used by giving their name to \C{elim} as in
+\C{elim/strong_nat_ind}. Still, strong induction is such a frequent
+proof step that the \mcbMC{} library provides dedicated idioms
+that we will detail in Section~\ref{sec:ubnP}.
+
+Finally, recall that recursive functions are checked for termination:
 Through the lenses of the proofs-as-programs correspondence, this means
 that the induction principle just coded is sound, i.e., based on a
 well-founded order relation.