2
Require Export ZArithRing.
4
(* Cette tactique a pour objectif de remplacer toute instance
5
de (POS (xI e)) ou de (POS (xO e)) par
6
2*(POS e)+1 ou 2*(POS e), pour rendre les expressions plus
7
� m�me d'�tre utilis�es par Ring, lorsque ces expressions contiennent
8
des variables de type positive. *)
11
| |- context [(Zpos (xI ?X1))] =>
14
| 1%positive => fail 1
15
| _ => rewrite (BinInt.Zpos_xI v)
17
| |- context [(Zpos (xO ?X1))] =>
20
| 1%positive => fail 1
21
| _ => rewrite (BinInt.Zpos_xO v)
25
Goal forall x : positive, Zpos (xI (xI x)) = (4 * Zpos x + 3)%Z.