+(* Here is our statement, where $\mathit{nat\_of\_bool}$ is the above coercions:
+*)
+
+lemma div2_ok: ∀n,q,r. div2 n = 〈q,r〉 → n = add (nat_of_bool r) (twice q).
+
+(* We proceed by induction on $n$, that produces two subgoals. *)
+
+#n elim n
+ [#q #r #H
+
+(* After introducing the hypothesis q,r and H, the first subgoal looks like the
+following:
+
+ n : nat
+ q : nat
+ r : bool
+ H : (div2 O=〈q,r〉)
+ ---------------------------
+
+ (O=add (nat_of_bool r) (twice q))
+
+Note that the right hand side of equation H is not in normal form, and we would
+like to reduce it. We can do it by specifying a pattern for the normalize
+tactic, introduced by the ``in'' keyword, and delimited by a semicolon. In this
+case, the pattern is just the name of the hypothesis and we should write *)
+
+ normalize in H;
+
+(* that transforms H as follows:
+
+ H : (〈O,ff〉=〈q,r〉)
+
+From such an hypothesis we expect to be able to conclude that q=O$ and r=false.
+The tactic that provides this functionality is called "destruct". The tactic
+decomposes an equality between structured terms in smaller components: if an
+absurd situation is recognized (like an equality between 0 and (S n)) the
+current goal is automatically closed; otherwise, all derived equations where one
+of the sides is a variable are automatically substituted in the proof, and the
+remaining equations are added to the context (replacing the original equation).
+
+In the above case, by invoking destruct we would get the two equations q=O and
+r=false; these are immediately substituted in the goal, that can now be solved
+by direct computation. *)
+
+ destruct //
+
+(********************************** Cut ***************************************)
+
+(* Let's come to the second subgoal *)
+ |#a #Hind #q #r
+(* After performing the previous introductions, the current goal looks like the
+following:
+
+ n : nat
+ a : nat
+ Hind : (∀q:nat.∀r:bool.div2 a=〈q,r〉→a=add (nat_of_bool r) (twice q))
+ q : nat
+ r : bool
+ ---------------------------
+ div2 (S a)=〈q,r〉→S a=add (nat_of_bool r) (twice q)
+
+We should proceed by cases on the remainder of (div2 a), but before doing it we
+should emphasize the fact that (div2 a) can be expressed as a pair of its two
+projections. The tactics that allows to introduce a new hypothesis, splitting a
+complex proofs into smaller components is called "cut".
+The invocation of "cut A" transforms the current goal G into the two subgoals A
+and A→G (A is called the cut formula).
+
+In our case, the cut formula is
+ div2 a = 〈fst … (div2 a), snd … (div2 a)〉
+whose proof is trivial
+*)
+