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)%ZThe 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.