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: Zorder.v,v 1.6.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
35 (*#* Binary Integers (Pierre Cr\233\gut (CNET, Lannion, France) *)
37 include "NArith/BinPos.ma".
39 include "ZArith/BinInt.ma".
41 include "Arith/Arith.ma".
43 include "Logic/Decidable.ma".
45 include "ZArith/Zcompare.ma".
48 Open Local Scope Z_scope.
52 Implicit Types x y z : Z.
55 (*#*********************************************************************)
57 (*#* Properties of the order relations on binary integers *)
61 inline procedural "cic:/Coq/ZArith/Zorder/Ztrichotomy_inf.con" as theorem.
63 inline procedural "cic:/Coq/ZArith/Zorder/Ztrichotomy.con" as theorem.
65 (*#*********************************************************************)
67 (*#* Decidability of equality and order on Z *)
69 inline procedural "cic:/Coq/ZArith/Zorder/dec_eq.con" as theorem.
71 inline procedural "cic:/Coq/ZArith/Zorder/dec_Zne.con" as theorem.
73 inline procedural "cic:/Coq/ZArith/Zorder/dec_Zle.con" as theorem.
75 inline procedural "cic:/Coq/ZArith/Zorder/dec_Zgt.con" as theorem.
77 inline procedural "cic:/Coq/ZArith/Zorder/dec_Zge.con" as theorem.
79 inline procedural "cic:/Coq/ZArith/Zorder/dec_Zlt.con" as theorem.
81 inline procedural "cic:/Coq/ZArith/Zorder/not_Zeq.con" as theorem.
83 (*#* Relating strict and large orders *)
85 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_lt.con" as lemma.
87 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_gt.con" as lemma.
89 inline procedural "cic:/Coq/ZArith/Zorder/Zge_le.con" as lemma.
91 inline procedural "cic:/Coq/ZArith/Zorder/Zle_ge.con" as lemma.
93 inline procedural "cic:/Coq/ZArith/Zorder/Zle_not_gt.con" as lemma.
95 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_not_le.con" as lemma.
97 inline procedural "cic:/Coq/ZArith/Zorder/Zle_not_lt.con" as lemma.
99 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_not_le.con" as lemma.
101 inline procedural "cic:/Coq/ZArith/Zorder/Znot_ge_lt.con" as lemma.
103 inline procedural "cic:/Coq/ZArith/Zorder/Znot_lt_ge.con" as lemma.
105 inline procedural "cic:/Coq/ZArith/Zorder/Znot_gt_le.con" as lemma.
107 inline procedural "cic:/Coq/ZArith/Zorder/Znot_le_gt.con" as lemma.
109 inline procedural "cic:/Coq/ZArith/Zorder/Zge_iff_le.con" as lemma.
111 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_iff_lt.con" as lemma.
115 inline procedural "cic:/Coq/ZArith/Zorder/Zle_refl.con" as lemma.
117 inline procedural "cic:/Coq/ZArith/Zorder/Zeq_le.con" as lemma.
120 Hint Resolve Zle_refl: zarith.
125 inline procedural "cic:/Coq/ZArith/Zorder/Zle_antisym.con" as lemma.
129 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_asym.con" as lemma.
131 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_asym.con" as lemma.
133 (*#* Irreflexivity *)
135 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_irrefl.con" as lemma.
137 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_irrefl.con" as lemma.
139 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_not_eq.con" as lemma.
141 (*#* Large = strict or equal *)
143 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_le_weak.con" as lemma.
145 inline procedural "cic:/Coq/ZArith/Zorder/Zle_lt_or_eq.con" as lemma.
149 inline procedural "cic:/Coq/ZArith/Zorder/Zle_or_lt.con" as lemma.
151 (*#* Transitivity of strict orders *)
153 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_trans.con" as lemma.
155 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_trans.con" as lemma.
157 (*#* Mixed transitivity *)
159 inline procedural "cic:/Coq/ZArith/Zorder/Zle_gt_trans.con" as lemma.
161 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_le_trans.con" as lemma.
163 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_le_trans.con" as lemma.
165 inline procedural "cic:/Coq/ZArith/Zorder/Zle_lt_trans.con" as lemma.
167 (*#* Transitivity of large orders *)
169 inline procedural "cic:/Coq/ZArith/Zorder/Zle_trans.con" as lemma.
171 inline procedural "cic:/Coq/ZArith/Zorder/Zge_trans.con" as lemma.
174 Hint Resolve Zle_trans: zarith.
177 (*#* Compatibility of successor wrt to order *)
179 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_le_compat.con" as lemma.
181 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_gt_compat.con" as lemma.
183 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_lt_compat.con" as lemma.
186 Hint Resolve Zsucc_le_compat: zarith.
189 (*#* Simplification of successor wrt to order *)
191 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_gt_reg.con" as lemma.
193 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_le_reg.con" as lemma.
195 inline procedural "cic:/Coq/ZArith/Zorder/Zsucc_lt_reg.con" as lemma.
197 (*#* Compatibility of addition wrt to order *)
199 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_gt_compat_l.con" as lemma.
201 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_gt_compat_r.con" as lemma.
203 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_compat_l.con" as lemma.
205 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_compat_r.con" as lemma.
207 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_compat_l.con" as lemma.
209 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_compat_r.con" as lemma.
211 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_le_compat.con" as lemma.
213 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_lt_compat.con" as lemma.
215 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_compat.con" as lemma.
217 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_compat.con" as lemma.
219 (*#* Compatibility of addition wrt to being positive *)
221 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con" as lemma.
223 (*#* Simplification of addition wrt to order *)
225 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_gt_reg_l.con" as lemma.
227 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_gt_reg_r.con" as lemma.
229 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_reg_l.con" as lemma.
231 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_le_reg_r.con" as lemma.
233 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_reg_l.con" as lemma.
235 inline procedural "cic:/Coq/ZArith/Zorder/Zplus_lt_reg_r.con" as lemma.
237 (*#* Special base instances of order *)
239 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_succ.con" as lemma.
241 inline procedural "cic:/Coq/ZArith/Zorder/Znot_le_succ.con" as lemma.
243 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_succ.con" as lemma.
245 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_pred.con" as lemma.
247 (*#* Relating strict and large order using successor or predecessor *)
249 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_le_succ.con" as lemma.
251 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_gt_succ.con" as lemma.
253 inline procedural "cic:/Coq/ZArith/Zorder/Zle_lt_succ.con" as lemma.
255 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_le_succ.con" as lemma.
257 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_succ_le.con" as lemma.
259 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_succ_le.con" as lemma.
261 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_succ_gt.con" as lemma.
263 (*#* Weakening order *)
265 inline procedural "cic:/Coq/ZArith/Zorder/Zle_succ.con" as lemma.
268 Hint Resolve Zle_succ: zarith.
271 inline procedural "cic:/Coq/ZArith/Zorder/Zle_pred.con" as lemma.
273 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_lt_succ.con" as lemma.
275 inline procedural "cic:/Coq/ZArith/Zorder/Zle_le_succ.con" as lemma.
277 inline procedural "cic:/Coq/ZArith/Zorder/Zle_succ_le.con" as lemma.
280 Hint Resolve Zle_le_succ: zarith.
283 (*#* Relating order wrt successor and order wrt predecessor *)
285 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_succ_pred.con" as lemma.
287 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_succ_pred.con" as lemma.
289 (*#* Relating strict order and large order on positive *)
291 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_0_le_0_pred.con" as lemma.
293 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_0_le_0_pred.con" as lemma.
295 (*#* Special cases of ordered integers *)
297 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_0_1.con" as lemma.
299 inline procedural "cic:/Coq/ZArith/Zorder/Zle_0_1.con" as lemma.
301 inline procedural "cic:/Coq/ZArith/Zorder/Zle_neg_pos.con" as lemma.
303 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_pos_0.con" as lemma.
305 (* weaker but useful (in [Zpower] for instance) *)
307 inline procedural "cic:/Coq/ZArith/Zorder/Zle_0_pos.con" as lemma.
309 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_neg_0.con" as lemma.
311 inline procedural "cic:/Coq/ZArith/Zorder/Zle_0_nat.con" as lemma.
314 Hint Immediate Zeq_le: zarith.
317 (*#* Transitivity using successor *)
319 inline procedural "cic:/Coq/ZArith/Zorder/Zge_trans_succ.con" as lemma.
321 (*#* Derived lemma *)
323 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_succ_gt_or_eq.con" as lemma.
325 (*#* Compatibility of multiplication by a positive wrt to order *)
327 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_compat_r.con" as lemma.
329 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_compat_l.con" as lemma.
331 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_compat_r.con" as lemma.
333 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_compat_r.con" as lemma.
335 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_compat_r.con" as lemma.
337 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_le_compat_r.con" as lemma.
339 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_0_le_compat_r.con" as lemma.
341 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_compat_l.con" as lemma.
343 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_compat_l.con" as lemma.
345 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_compat_l.con" as lemma.
347 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_ge_compat_r.con" as lemma.
349 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_ge_compat_l.con" as lemma.
351 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_ge_compat.con" as lemma.
353 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_compat.con" as lemma.
355 (*#* Simplification of multiplication by a positive wrt to being positive *)
357 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_reg_r.con" as lemma.
359 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_reg_r.con" as lemma.
361 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_reg_r.con" as lemma.
363 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_0_le_reg_r.con" as lemma.
365 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_ge_reg_r.con" as lemma.
367 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_reg_r.con" as lemma.
369 (*#* Compatibility of multiplication by a positive wrt to being positive *)
371 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_0_compat.con" as lemma.
373 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_compat.con" as lemma.
375 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_O_compat.con" as lemma.
377 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_le_0_compat.con" as lemma.
379 (*#* Simplification of multiplication by a positive wrt to being positive *)
381 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_le_0_reg_r.con" as lemma.
383 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_lt_0_reg_r.con" as lemma.
385 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_lt_0_reg_r.con" as lemma.
387 inline procedural "cic:/Coq/ZArith/Zorder/Zmult_gt_0_reg_l.con" as lemma.
389 (*#* Simplification of square wrt order *)
391 inline procedural "cic:/Coq/ZArith/Zorder/Zgt_square_simpl.con" as lemma.
393 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_square_simpl.con" as lemma.
395 (*#* Equivalence between inequalities *)
397 inline procedural "cic:/Coq/ZArith/Zorder/Zle_plus_swap.con" as lemma.
399 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_plus_swap.con" as lemma.
401 inline procedural "cic:/Coq/ZArith/Zorder/Zeq_plus_swap.con" as lemma.
403 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_minus_simpl_swap.con" as lemma.
405 inline procedural "cic:/Coq/ZArith/Zorder/Zlt_O_minus_lt.con" as lemma.