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

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

Require Omega.
Require Le_omega.

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

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

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

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

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

Theorem lt_n_O : (n:nat)~(lt n O).
Proof le_Sn_O.
Hints Resolve lt_n_O : arith.

Theorem lt_n_n : (n:nat)~(lt n n).
Proof le_Sn_n.
Hints Resolve lt_n_n : arith.

Lemma S_pred : (n,m:nat)(lt m n)->(n=(S (pred n))).
Proof.
Induction 1; Auto with arith v62.
(*
Omega does not recognize pred and fails
*)
Qed.

Lemma lt_pred : (n,p:nat)(lt (S n) p)->(lt n (pred p)).
Proof.
Induction 1; Simpl; Auto with arith v62.
(*
Omega does not recognize pred and fails too
*)
Qed.
Hints Immediate lt_pred : arith.

Lemma lt_pred_n_n : (n:nat)(lt O n)->(lt (pred n) n).
Proof.
Destruct 1; Simpl; Auto with arith v62.
(*
Omega does not recognize pred and fails too
*)
Qed.
Hints Resolve lt_pred_n_n : arith.

(* Relationship between le and lt *) 

Theorem lt_le_S : (n,p:nat)(lt n p)->(le (S n) p).
Proof.
Intros; Omega.
Qed.
Hints Immediate lt_le_S : arith.

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

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

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

Theorem neq_O_lt : (n:nat)(~O=n)->(lt O n).
Proof.
Intros; Omega.
Qed.
Hints Immediate neq_O_lt : arith.

Theorem lt_O_neq : (n:nat)(lt O n)->(~O=n).
Proof.
Intros; Omega.
Qed.
Hints Immediate lt_O_neq : arith.

(* Transitivity properties *)

Theorem lt_trans : (n,m,p:nat)(lt n m)->(lt m p)->(lt n p).
Proof.
Intros; Omega.
Qed.

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

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

Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m).
Proof.
Intros; Omega.
Qed.

Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)).
Proof.
Intros; Omega.
Qed.

Theorem le_not_lt : (n,m:nat)(le n m)->~(lt m n).
Proof.
Intros; Omega.
Qed.
Hints Immediate le_not_lt : arith.

Theorem lt_not_le : (n,m:nat)(lt n m)->~(le m n).
Proof.
Intros; Omega.
Qed.
Hints Immediate lt_not_le : arith.

Theorem lt_not_sym : (n,m:nat)(lt n m)->~(lt m n).
Proof.
Intros; Omega.
Qed.

Theorem nat_total_order: (m, n: nat) ~ m = n -> (lt m n) \/ (lt n m).
Proof.
Intros; Omega.
Qed.


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