+
+(* 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 *)