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: Plus.v,v 1.18.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
35 (*#* Properties of addition *)
37 include "Arith/Le.ma".
39 include "Arith/Lt.ma".
42 Open Local Scope nat_scope.
46 Implicit Types m n p q : nat.
49 (*#* Zero is neutral *)
51 inline procedural "cic:/Coq/Arith/Plus/plus_0_l.con" as lemma.
53 inline procedural "cic:/Coq/Arith/Plus/plus_0_r.con" as lemma.
57 inline procedural "cic:/Coq/Arith/Plus/plus_comm.con" as lemma.
60 Hint Immediate plus_comm: arith v62.
65 inline procedural "cic:/Coq/Arith/Plus/plus_Snm_nSm.con" as lemma.
67 inline procedural "cic:/Coq/Arith/Plus/plus_assoc.con" as lemma.
70 Hint Resolve plus_assoc: arith v62.
73 inline procedural "cic:/Coq/Arith/Plus/plus_permute.con" as lemma.
75 inline procedural "cic:/Coq/Arith/Plus/plus_assoc_reverse.con" as lemma.
78 Hint Resolve plus_assoc_reverse: arith v62.
81 (*#* Simplification *)
83 inline procedural "cic:/Coq/Arith/Plus/plus_reg_l.con" as lemma.
85 inline procedural "cic:/Coq/Arith/Plus/plus_le_reg_l.con" as lemma.
87 inline procedural "cic:/Coq/Arith/Plus/plus_lt_reg_l.con" as lemma.
89 (*#* Compatibility with order *)
91 inline procedural "cic:/Coq/Arith/Plus/plus_le_compat_l.con" as lemma.
94 Hint Resolve plus_le_compat_l: arith v62.
97 inline procedural "cic:/Coq/Arith/Plus/plus_le_compat_r.con" as lemma.
100 Hint Resolve plus_le_compat_r: arith v62.
103 inline procedural "cic:/Coq/Arith/Plus/le_plus_l.con" as lemma.
106 Hint Resolve le_plus_l: arith v62.
109 inline procedural "cic:/Coq/Arith/Plus/le_plus_r.con" as lemma.
112 Hint Resolve le_plus_r: arith v62.
115 inline procedural "cic:/Coq/Arith/Plus/le_plus_trans.con" as theorem.
118 Hint Resolve le_plus_trans: arith v62.
121 inline procedural "cic:/Coq/Arith/Plus/lt_plus_trans.con" as theorem.
124 Hint Immediate lt_plus_trans: arith v62.
127 inline procedural "cic:/Coq/Arith/Plus/plus_lt_compat_l.con" as lemma.
130 Hint Resolve plus_lt_compat_l: arith v62.
133 inline procedural "cic:/Coq/Arith/Plus/plus_lt_compat_r.con" as lemma.
136 Hint Resolve plus_lt_compat_r: arith v62.
139 inline procedural "cic:/Coq/Arith/Plus/plus_le_compat.con" as lemma.
141 inline procedural "cic:/Coq/Arith/Plus/plus_le_lt_compat.con" as lemma.
143 inline procedural "cic:/Coq/Arith/Plus/plus_lt_le_compat.con" as lemma.
145 inline procedural "cic:/Coq/Arith/Plus/plus_lt_compat.con" as lemma.
147 (*#* Inversion lemmas *)
149 inline procedural "cic:/Coq/Arith/Plus/plus_is_O.con" as lemma.
151 inline procedural "cic:/Coq/Arith/Plus/plus_is_one.con" as definition.
153 (*#* Derived properties *)
155 inline procedural "cic:/Coq/Arith/Plus/plus_permute_2_in_4.con" as lemma.
157 (*#* Tail-recursive plus *)
159 (*#* [tail_plus] is an alternative definition for [plus] which is
160 tail-recursive, whereas [plus] is not. This can be useful
161 when extracting programs. *)
163 inline procedural "cic:/Coq/Arith/Plus/plus_acc.con" as definition.
165 inline procedural "cic:/Coq/Arith/Plus/tail_plus.con" as definition.
167 inline procedural "cic:/Coq/Arith/Plus/plus_tail_plus.con" as lemma.