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

Require Le.
Require Lt.

Theorem zerop : (n:nat){n=O}+{lt O n}.
Destruct n; Auto.
Save.

Theorem lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}.
Proof.
Induction n; Induction m; Auto.
Intros q H'; Elim (H q).
Induction 1; Auto.
Auto.
Qed.

Lemma gt_eq_gt_dec : (n,m:nat)({(gt m n)}+{n=m})+{(gt n m)}.
Proof lt_eq_lt_dec.

Lemma le_lt_dec : (n,m:nat) {le n m} + {lt m n}.
Proof.
Induction n.
Auto.
Induction m.
Auto.
Intros q H'; Elim (H q); Auto.
Qed.

Lemma le_le_S_dec : (n,m:nat) {le n m} + {le (S m) n}.
Proof le_lt_dec.

Lemma le_ge_dec : (n,m:nat) {le n m} + {ge n m}.
Proof.
Intros; Elim (le_lt_dec n m); Auto.
Qed.

Theorem le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}.
Proof le_lt_dec.


Theorem le_lt_eq_dec : (n,m:nat)(le n m)->({(lt n m)}+{n=m}).
Proof.
Intros; Elim (lt_eq_lt_dec n m); Auto.
Intros; Absurd (lt m n); Auto.
Qed.


(* $Id: Compare_dec.v,v 1.4 1998/04/30 16:45:43 mohring Exp $ *)
