(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                                  Plus.v                                  *)
(****************************************************************************)


(************************************************************************)
(*  Properties of addition                                              *)
(************************************************************************)

(* All theorems of Plus.v are solvable by Omega                         *)
Require Omega.

Lemma plus_sym : (n,m:nat)((plus n m)=(plus m n)).
Proof.
Intros; Omega.
Qed.
Hints Immediate plus_sym : arith.

Lemma plus_Snm_nSm : 
  (n,m:nat)(plus (S n) m)=(plus n (S m)).
Proof.
Intros; Omega.
Qed.

Lemma simpl_plus_l : (n,m,p:nat)((plus n m)=(plus n p))->(m=p).
Proof.
Intros; Omega.
Qed.

Lemma plus_assoc_l : (n,m,p:nat)((plus n (plus m p))=(plus (plus n m) p)).
Proof.
Intros; Omega.
Qed.
Hints Resolve plus_assoc_l : arith.

Lemma plus_permute : (n,m,p:nat) ((plus n (plus m p))=(plus m (plus n p))).
Proof. 
Intros; Omega.
Qed.

Lemma plus_assoc_r : (n,m,p:nat)((plus (plus n m) p)=(plus n (plus m p))).
Proof.
Intros; Omega.
Qed.
Hints Resolve plus_assoc_r : arith.

Lemma simpl_le_plus_l : (p,n,m:nat)(le (plus p n) (plus p m))->(le n m).
Proof.
Intros; Omega.
Qed.

Lemma le_reg_l : (n,m,p:nat)(le n m)->(le (plus p n) (plus p m)).
Proof.
Intros; Omega.
Qed.
Hints Resolve le_reg_l : arith.

Lemma le_reg_r : (a,b,c:nat) (le a b)->(le (plus a c) (plus b c)).
Proof.
Intros; Omega.
Qed.
Hints Resolve le_reg_r : arith.

Lemma le_plus_plus : 
	(n,m,p,q:nat) (le n m)->(le p q)->(le (plus n p) (plus m q)).
Proof.
Intros; Omega.
Qed.

Lemma le_plus_l : (n,m:nat)(le n (plus n m)).
Proof.
Intros; Omega.
Qed.
Hints Resolve le_plus_l : arith.

Lemma le_plus_r : (n,m:nat)(le m (plus n m)).
Proof.
Intros; Omega.
Qed.
Hints Resolve le_plus_r : arith.

Theorem le_plus_trans : (n,m,p:nat)(le n m)->(le n (plus m p)).
Proof.
Intros; Omega.
Qed.
Hints Resolve le_plus_trans : arith.

Require Lt.

Lemma simpl_lt_plus_l : (n,m,p:nat)(lt (plus p n) (plus p m))->(lt n m).
Proof.
Intros; Omega.
Qed.

Lemma lt_reg_l : (n,m,p:nat)(lt n m)->(lt (plus p n) (plus p m)).
Proof.
Intros; Omega.
Qed.
Hints Resolve lt_reg_l : arith.

Lemma lt_reg_r : (n,m,p:nat)(lt n m) -> (lt (plus n p) (plus m p)).
Proof.
Intros; Omega.
Qed.
Hints Resolve lt_reg_r : arith.

Theorem lt_plus_trans : (n,m,p:nat)(lt n m)->(lt n (plus m p)).
Proof.
Intros; Omega.
Qed.
Hints Immediate lt_plus_trans : arith.



(* $Id: Plus_omega.v,v 1.3 1999/06/29 13:09:06 loiseleu Exp $ *)
