(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                                   Le.v                                   *)
(****************************************************************************)

(***************************************)
(* Order on natural numbers            *)
(***************************************)


(* Omega solves all theorems of Le.v except the ones mentionning the        *) 
(* predecessor on natural numbers and le_elim_rel which mentions an         *)
(* arbitrary undecidable predicate                                          *)

Require Omega.

Section less_or_equal.
Variable n,m,p:nat.

Theorem le_n_S : (le n m)->(le (S n) (S m)).
Proof.
Omega.
Qed.

Theorem le_trans : (le n m)->(le m p)->(le n p).
Proof.
Omega.
Qed.

Theorem le_n_Sn : (le n (S n)).
Proof.
Omega.
Qed.

Theorem le_O_n : (le O n).
Proof.
Omega.
Qed.

End less_or_equal.
Hint le_n_S le_n_Sn le_O_n.

Theorem le_pred_n : (n:nat)(le (pred n) n).
Proof.
(*
Intros;Omega.
... Omega do not recognize predecessor on natural numbers ... and fails
*)
Induction n ; Auto.
Qed.
Hint le_pred_n.

Theorem le_trans_S : (n,m:nat)(le (S n) m)->(le n m).
Proof.
Intros; Omega.
(* Omega applies to unquantified formulas: Intros first is necessary *)
Qed.
Immediate le_trans_S.

Theorem le_S_n : (n,m:nat)(le (S n) (S m))->(le n m).
Proof.
Intros; Omega.
Qed.
Immediate le_S_n.

(* Negative properties *)

Theorem le_Sn_O : (n:nat)~(le (S n) O).
Proof.
Intros; Omega.
Qed.
Hint le_Sn_O.

Theorem le_Sn_n : (n:nat)~(le (S n) n).
Proof.
Intros; Omega.
Qed.
Hint le_Sn_n.

Theorem le_antisym : (n,m:nat)(le n m)->(le m n)->(n=m).
Proof.
Intros; Omega.
Qed.
Immediate le_antisym.

Theorem le_n_O_eq : (n:nat)(le n O)->(O=n).
Proof.
Intros; Omega.
Qed.
Immediate le_n_O_eq.


(* A different elimination principle for the order on natural numbers *)

Lemma le_elim_rel : (P:nat->nat->Prop)
     ((p:nat)(P O p))->
     ((p,q:nat)(le p q)->(P p q)->(P (S p) (S q)))->
     (n,m:nat)(le n m)->(P n m).
Proof.
(*
Intros; Omega.
... Omega treat only statements of arithmetic (built on connectors ->,
\/, /\, ~, False, True and on arithmetical predicates =, <=, <, >=, >).
Here, P is not one of these predefined (and decidable) predicates.
*)
Induction n; Trivial.
Intros n' HRec m Le.
Elim Le; Auto.
Qed.


(* $Id: Le_omega.v,v 1.1 1998/07/02 13:22:16 loiseleu Exp $ *)
