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: Minus.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
35 (*#* Subtraction (difference between two natural numbers) *)
37 include "Arith/Lt.ma".
39 include "Arith/Le.ma".
42 Open Local Scope nat_scope.
46 Implicit Types m n p : nat.
49 (*#* 0 is right neutral *)
51 inline procedural "cic:/Coq/Arith/Minus/minus_n_O.con" as lemma.
54 Hint Resolve minus_n_O: arith v62.
57 (*#* Permutation with successor *)
59 inline procedural "cic:/Coq/Arith/Minus/minus_Sn_m.con" as lemma.
62 Hint Resolve minus_Sn_m: arith v62.
65 inline procedural "cic:/Coq/Arith/Minus/pred_of_minus.con" as theorem.
69 inline procedural "cic:/Coq/Arith/Minus/minus_n_n.con" as lemma.
72 Hint Resolve minus_n_n: arith v62.
75 (*#* Simplification *)
77 inline procedural "cic:/Coq/Arith/Minus/minus_plus_simpl_l_reverse.con" as lemma.
80 Hint Resolve minus_plus_simpl_l_reverse: arith v62.
83 (*#* Relation with plus *)
85 inline procedural "cic:/Coq/Arith/Minus/plus_minus.con" as lemma.
88 Hint Immediate plus_minus: arith v62.
91 inline procedural "cic:/Coq/Arith/Minus/minus_plus.con" as lemma.
94 Hint Resolve minus_plus: arith v62.
97 inline procedural "cic:/Coq/Arith/Minus/le_plus_minus.con" as lemma.
100 Hint Resolve le_plus_minus: arith v62.
103 inline procedural "cic:/Coq/Arith/Minus/le_plus_minus_r.con" as lemma.
106 Hint Resolve le_plus_minus_r: arith v62.
109 (*#* Relation with order *)
111 inline procedural "cic:/Coq/Arith/Minus/le_minus.con" as theorem.
113 inline procedural "cic:/Coq/Arith/Minus/lt_minus.con" as lemma.
116 Hint Resolve lt_minus: arith v62.
119 inline procedural "cic:/Coq/Arith/Minus/lt_O_minus_lt.con" as lemma.
122 Hint Immediate lt_O_minus_lt: arith v62.
125 inline procedural "cic:/Coq/Arith/Minus/not_le_minus_0.con" as theorem.