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

Require Import GenericTactics.
Require Export Arith.

Lemma plus_n_0 : forall n, n + 0 = n.
intuition.
Qed.

Lemma plus_0_n : forall n, 0 + n = n.
intuition.
Qed.

Hint Rewrite plus_n_0 plus_0_n : rew_db.