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

(* Omega solves all theorems of Gt.v except the ones mentionning the        *) 
(* predecessor on natural numbers                                           *)

Require Omega.
Require Le_omega.
Require Lt_omega.

Theorem gt_Sn_O : (n:nat)(gt (S n) O).
Proof.
Intros; Omega.
Qed.
Hints Resolve gt_Sn_O : arith.

Theorem gt_Sn_n : (n:nat)(gt (S n) n).
Proof.
Intros; Omega.
Qed.
Hints Resolve gt_Sn_n : arith.

Theorem le_S_gt : (n,m:nat)(le (S n) m)->(gt m n).
Proof.
Intros; Omega.
Qed.
Hints Immediate le_S_gt : arith.

Theorem gt_n_S : (n,m:nat)(gt n m)->(gt (S n) (S m)).
Proof.
Intros; Omega.
Qed.
Hints Resolve gt_n_S : arith.

Theorem gt_trans_S : (n,m,p:nat)(gt (S n) m)->(gt m p)->(gt n p).
Proof.
Intros; Omega.
Qed.

Theorem le_gt_trans : (n,m,p:nat)(le m n)->(gt m p)->(gt n p).
Proof.
Intros; Omega.
Qed.

Theorem gt_le_trans : (n,m,p:nat)(gt n m)->(le p m)->(gt n p).
Proof.
Intros; Omega.
Qed.

Lemma le_not_gt : (n,m:nat)(le n m)->~(gt n m).
Proof le_not_lt.
Hints Resolve le_not_gt : arith.

Lemma gt_antirefl : (n:nat)~(gt n n).
Proof lt_n_n.
Hints Resolve gt_antirefl : arith.

Lemma gt_not_sym : (n,m:nat)(gt n m)->~(gt m n).
Proof [n,m:nat](lt_not_sym m n).

Lemma gt_not_le : (n,m:nat)(gt n m)->~(le n m).
Proof.
Intros; Omega.
Qed.
Hints Resolve gt_not_le : arith.

Lemma gt_trans : (n,m,p:nat)(gt n m)->(gt m p)->(gt n p).
Proof.
Intros; Omega.
Qed.

Lemma gt_S_n : (n,p:nat)(gt (S p) (S n))->(gt p n).
Proof.
Intros; Omega.
Qed.
Hints Immediate gt_S_n : arith.

Lemma gt_S_le : (n,p:nat)(gt (S p) n)->(le n p).
Proof.
Intros; Omega.
Qed.
Hints Immediate gt_S_le : arith.

Lemma gt_le_S : (n,p:nat)(gt p n)->(le (S n) p).
Proof.
Intros; Omega.
Qed.
Hints Resolve gt_le_S : arith.

Lemma le_gt_S : (n,p:nat)(le n p)->(gt (S p) n).
Proof.
Intros; Omega.
Qed.
Hints Resolve le_gt_S : arith.

Lemma gt_pred : (n,p:nat)(gt p (S n))->(gt (pred p) n).
Proof.
Auto with arith v62.
(* Omega does not recognize pred and fails *)
Qed.
Hints Immediate gt_pred : arith.

Theorem gt_S : (n,m:nat)(gt (S n) m)->((gt n m)\/(<nat>m=n)).
Proof.
Intros; Omega.
Qed.

Theorem gt_O_eq : (n:nat)((gt n O)\/(<nat>O=n)).
Proof.
Intros; Omega.
Qed.

Require Plus.

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

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


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