blob: 4b3d18be4bf9c68d0bc1f906e357a6210f93bb82 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
(*i $Id$ i*)
Require Export NZAxioms.
Set Implicit Arguments.
Module Type ZAxiomsSig.
Include Type NZOrdAxiomsSig.
Local Open Scope NumScope.
Parameter Inline opp : t -> t.
Declare Instance opp_wd : Proper (eq==>eq) opp.
Notation "- x" := (opp x) (at level 35, right associativity) : NumScope.
Notation "- 1" := (- (1)) : NumScope.
(* Integers are obtained by postulating that every number has a predecessor *)
Axiom succ_pred : forall n, S (P n) == n.
Axiom opp_0 : - 0 == 0.
Axiom opp_succ : forall n, - (S n) == P (- n).
End ZAxiomsSig.
|
