# Rewriting with exceptions

The `ZArith` library provides the following two theorems:

Zpos_xI : forall p:positive, Zpos (xI p) = (2 * Zpos p + 1)%Z
Zpos_xO : forall p:positive, Zpos (xO p) = (2 * Zpos p)%Z

The number `2%Z` is also represented by `Zpos (xO xH)`. Write
a function that rewrite as many times as possible with these two theorems
without entering a loop.

## Solution

Look at this file
Yves Bertot
Last modified: Sun May 8 08:06:46 MEST 2005