1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Lt.v,v 1.11.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
35 include "Arith/Le.ma".
38 Open Local Scope nat_scope.
42 Implicit Types m n p : nat.
47 inline procedural "cic:/Coq/Arith/Lt/lt_irrefl.con" as theorem.
50 Hint Resolve lt_irrefl: arith v62.
53 (*#* Relationship between [le] and [lt] *)
55 inline procedural "cic:/Coq/Arith/Lt/lt_le_S.con" as theorem.
58 Hint Immediate lt_le_S: arith v62.
61 inline procedural "cic:/Coq/Arith/Lt/lt_n_Sm_le.con" as theorem.
64 Hint Immediate lt_n_Sm_le: arith v62.
67 inline procedural "cic:/Coq/Arith/Lt/le_lt_n_Sm.con" as theorem.
70 Hint Immediate le_lt_n_Sm: arith v62.
73 inline procedural "cic:/Coq/Arith/Lt/le_not_lt.con" as theorem.
75 inline procedural "cic:/Coq/Arith/Lt/lt_not_le.con" as theorem.
78 Hint Immediate le_not_lt lt_not_le: arith v62.
83 inline procedural "cic:/Coq/Arith/Lt/lt_asym.con" as theorem.
85 (*#* Order and successor *)
87 inline procedural "cic:/Coq/Arith/Lt/lt_n_Sn.con" as theorem.
90 Hint Resolve lt_n_Sn: arith v62.
93 inline procedural "cic:/Coq/Arith/Lt/lt_S.con" as theorem.
96 Hint Resolve lt_S: arith v62.
99 inline procedural "cic:/Coq/Arith/Lt/lt_n_S.con" as theorem.
102 Hint Resolve lt_n_S: arith v62.
105 inline procedural "cic:/Coq/Arith/Lt/lt_S_n.con" as theorem.
108 Hint Immediate lt_S_n: arith v62.
111 inline procedural "cic:/Coq/Arith/Lt/lt_O_Sn.con" as theorem.
114 Hint Resolve lt_O_Sn: arith v62.
117 inline procedural "cic:/Coq/Arith/Lt/lt_n_O.con" as theorem.
120 Hint Resolve lt_n_O: arith v62.
125 inline procedural "cic:/Coq/Arith/Lt/S_pred.con" as lemma.
127 inline procedural "cic:/Coq/Arith/Lt/lt_pred.con" as lemma.
130 Hint Immediate lt_pred: arith v62.
133 inline procedural "cic:/Coq/Arith/Lt/lt_pred_n_n.con" as lemma.
136 Hint Resolve lt_pred_n_n: arith v62.
139 (*#* Transitivity properties *)
141 inline procedural "cic:/Coq/Arith/Lt/lt_trans.con" as theorem.
143 inline procedural "cic:/Coq/Arith/Lt/lt_le_trans.con" as theorem.
145 inline procedural "cic:/Coq/Arith/Lt/le_lt_trans.con" as theorem.
148 Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62.
151 (*#* Large = strict or equal *)
153 inline procedural "cic:/Coq/Arith/Lt/le_lt_or_eq.con" as theorem.
155 inline procedural "cic:/Coq/Arith/Lt/lt_le_weak.con" as theorem.
158 Hint Immediate lt_le_weak: arith v62.
163 inline procedural "cic:/Coq/Arith/Lt/le_or_lt.con" as theorem.
165 inline procedural "cic:/Coq/Arith/Lt/nat_total_order.con" as theorem.
167 (*#* Comparison to 0 *)
169 inline procedural "cic:/Coq/Arith/Lt/neq_O_lt.con" as theorem.
172 Hint Immediate neq_O_lt: arith v62.
175 inline procedural "cic:/Coq/Arith/Lt/lt_O_neq.con" as theorem.
178 Hint Immediate lt_O_neq: arith v62.