(* AUTEURS / AUTHORS :                          *)
(* Judicaël Courant,   Jean-François Monin      *)
(* VERIMAG, Université Joseph Fourier, Grenoble *)
(*                                         2006 *)

Require Import GenericTactics.
Require Export ZArith.

(* Some useful arithmetic result for rewriting *)

Lemma plus_z_0 : forall z, z + 0 = z.
intuition.
Qed.

Lemma plus_0_z : forall z, 0 + z = z.
intuition.
Qed.

Hint Rewrite plus_z_0 plus_0_z inj_plus inj_S : rew_db.