diff options
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 119 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 95 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 117 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 306 |
4 files changed, 519 insertions, 118 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 934fbc4280..d2f9b0a024 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -11,50 +11,99 @@ (*i $Id$ i*) Require Export BigN. +Require Import ZTimesOrder. +Require Import ZSig. +Require Import ZSigZAxioms. Require Import ZMake. +Module BigZ <: ZType := ZMake.Make BigN. -Module BigZ := Make BigN. +(** Module [BigZ] implements [ZAxiomsSig] *) +Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ. +Module Export BigZTimesOrderPropMod := ZTimesOrderPropFunct BigZAxiomsMod. -Definition bigZ := BigZ.t. +(** Notations about [BigZ] *) + +Notation bigZ := BigZ.t. Delimit Scope bigZ_scope with bigZ. Bind Scope bigZ_scope with bigZ. Bind Scope bigZ_scope with BigZ.t. Bind Scope bigZ_scope with BigZ.t_. -Notation " i + j " := (BigZ.add i j) : bigZ_scope. -Notation " i - j " := (BigZ.sub i j) : bigZ_scope. -Notation " i * j " := (BigZ.mul i j) : bigZ_scope. -Notation " i / j " := (BigZ.div i j) : bigZ_scope. -Notation " i ?= j " := (BigZ.compare i j) : bigZ_scope. - - - Theorem spec_to_Z: - forall n, BigN.to_Z (BigZ.to_N n) = - (Zsgn (BigZ.to_Z n) * BigZ.to_Z n)%Z. - intros n; case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. - intros p1 H1; case H1; auto. - intros p1 H1; case H1; auto. - Qed. - - Theorem spec_to_N n: - (BigZ.to_Z n = - Zsgn (BigZ.to_Z n) * (BigN.to_Z (BigZ.to_N n)))%Z. - intros n; case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. - intros p1 H1; case H1; auto. - intros p1 H1; case H1; auto. - Qed. - - Theorem spec_to_Z_pos: - forall n, (0 <= BigZ.to_Z n -> - BigN.to_Z (BigZ.to_N n) = BigZ.to_Z n)%Z. - intros n; case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. - intros p1 _ H1; case H1; auto. - intros p1 H1; case H1; auto. - Qed. +Notation Local "0" := BigZ.zero : bigZ_scope. +Infix "+" := BigZ.add : bigZ_scope. +Infix "-" := BigZ.sub : bigZ_scope. +Notation "- x" := (BigZ.opp x) : bigZ_scope. +Infix "*" := BigZ.mul : bigZ_scope. +Infix "/" := BigZ.div : bigZ_scope. +Infix "?=" := BigZ.compare : bigZ_scope. +Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope. +Infix "<" := BigZ.lt : bigZ_scope. +Infix "<=" := BigZ.le : bigZ_scope. +Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. + +Open Scope bigZ_scope. + +(** Some additional results about [BigZ] *) + +Theorem spec_to_Z: forall n:bigZ, + BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z. +Proof. +intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. +intros p1 H1; case H1; auto. +intros p1 H1; case H1; auto. +Qed. + +Theorem spec_to_N n: + ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. +Proof. +intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. +intros p1 H1; case H1; auto. +intros p1 H1; case H1; auto. +Qed. + +Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z -> + BigN.to_Z (BigZ.to_N n) = [n]. +Proof. +intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. +intros p1 _ H1; case H1; auto. +intros p1 H1; case H1; auto. +Qed. + +Lemma sub_opp : forall x y : bigZ, x - y == x + (- y). +Proof. +red; intros; zsimpl; auto. +Qed. + +Lemma plus_opp : forall x : bigZ, x + (- x) == 0. +Proof. +red; intros; zsimpl; auto with zarith. +Qed. + +(** [BigZ] is a ring *) + +Lemma BigZring : + ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq. +Proof. +constructor. +exact Zplus_0_l. +exact Zplus_comm. +exact Zplus_assoc. +exact Ztimes_1_l. +exact Ztimes_comm. +exact Ztimes_assoc. +exact Ztimes_plus_distr_r. +exact sub_opp. +exact plus_opp. +Qed. + +Add Ring BigZr : BigZring. + +(** Todo: tactic translating from [BigZ] to [Z] + omega *) +(** Todo: micromega *) diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 83171388d9..cbf6f701f2 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -12,94 +12,18 @@ Require Import ZArith. Require Import BigNumPrelude. +Require Import NSig. +Require Import ZSig. Open Scope Z_scope. -Module Type NType. - - Parameter t : Type. - - Parameter zero : t. - Parameter one : t. - - Parameter of_N : N -> t. - Parameter to_Z : t -> Z. - Parameter spec_pos: forall x, 0 <= to_Z x. - Parameter spec_0: to_Z zero = 0. - Parameter spec_1: to_Z one = 1. - Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x. - - Parameter compare : t -> t -> comparison. - - Parameter spec_compare: forall x y, - match compare x y with - Eq => to_Z x = to_Z y - | Lt => to_Z x < to_Z y - | Gt => to_Z x > to_Z y - end. - - Parameter eq_bool : t -> t -> bool. - - Parameter spec_eq_bool: forall x y, - if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y. - - Parameter succ : t -> t. - - Parameter spec_succ: forall n, to_Z (succ n) = to_Z n + 1. - - Parameter add : t -> t -> t. - - Parameter spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. - - Parameter pred : t -> t. - - Parameter spec_pred: forall x, 0 < to_Z x -> to_Z (pred x) = to_Z x - 1. - - Parameter sub : t -> t -> t. - - Parameter spec_sub: forall x y, to_Z y <= to_Z x -> - to_Z (sub x y) = to_Z x - to_Z y. - - Parameter mul : t -> t -> t. - - Parameter spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y. - - Parameter square : t -> t. - - Parameter spec_square: forall x, to_Z (square x) = to_Z x * to_Z x. - - Parameter power_pos : t -> positive -> t. - - Parameter spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n. - - Parameter sqrt : t -> t. - - Parameter spec_sqrt: forall x, to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2. - - Parameter div_eucl : t -> t -> t * t. - - Parameter spec_div_eucl: forall x y, - 0 < to_Z y -> - let (q,r) := div_eucl x y in (to_Z q, to_Z r) = (Zdiv_eucl (to_Z x) (to_Z y)). +(** * ZMake - Parameter div : t -> t -> t. - - Parameter spec_div: forall x y, - 0 < to_Z y -> to_Z (div x y) = to_Z x / to_Z y. - - Parameter modulo : t -> t -> t. - - Parameter spec_modulo: - forall x y, 0 < to_Z y -> to_Z (modulo x y) = to_Z x mod to_Z y. - - Parameter gcd : t -> t -> t. - - Parameter spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b). - - -End NType. + A generic transformation from a structure of natural numbers + [NSig.NType] to a structure of integers [ZSig.ZType]. +*) -Module Make (N:NType). +Module Make (N:NType) <: ZType. Inductive t_ := | Pos : N.t -> t_ @@ -131,6 +55,7 @@ Module Make (N:NType). intros; rewrite N.spec_of_N; auto. Qed. + Definition eq x y := (to_Z x = to_Z y). Theorem spec_0: to_Z zero = 0. exact N.spec_0. @@ -160,6 +85,10 @@ Module Make (N:NType). | Neg nx, Neg ny => N.compare ny nx end. + Definition lt n m := compare n m = Lt. + Definition le n m := compare n m <> Gt. + Definition min n m := match compare n m with Gt => m | _ => n end. + Definition max n m := match compare n m with Lt => m | _ => n end. Theorem spec_compare: forall x y, match compare x y with diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v new file mode 100644 index 0000000000..4e45939831 --- /dev/null +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -0,0 +1,117 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) + +Require Import ZArith Znumtheory. + +Open Scope Z_scope. + +(** * ZSig *) + +(** Interface of a rich structure about integers. + Specifications are written via translation to Z. +*) + +Module Type ZType. + + Parameter t : Type. + + Parameter to_Z : t -> Z. + Notation "[ x ]" := (to_Z x). + + Definition eq x y := ([x] = [y]). + + Parameter of_Z : Z -> t. + Parameter spec_of_Z: forall x, to_Z (of_Z x) = x. + + Parameter zero : t. + Parameter one : t. + Parameter minus_one : t. + + Parameter spec_0: [zero] = 0. + Parameter spec_1: [one] = 1. + Parameter spec_m1: [minus_one] = -1. + + Parameter compare : t -> t -> comparison. + + Parameter spec_compare: forall x y, + match compare x y with + | Eq => [x] = [y] + | Lt => [x] < [y] + | Gt => [x] > [y] + end. + + Definition lt n m := compare n m = Lt. + Definition le n m := compare n m <> Gt. + Definition min n m := match compare n m with Gt => m | _ => n end. + Definition max n m := match compare n m with Lt => m | _ => n end. + + Parameter eq_bool : t -> t -> bool. + + Parameter spec_eq_bool: forall x y, + if eq_bool x y then [x] = [y] else [x] <> [y]. + + Parameter succ : t -> t. + + Parameter spec_succ: forall n, [succ n] = [n] + 1. + + Parameter add : t -> t -> t. + + Parameter spec_add: forall x y, [add x y] = [x] + [y]. + + Parameter pred : t -> t. + + Parameter spec_pred: forall x, [pred x] = [x] - 1. + + Parameter sub : t -> t -> t. + + Parameter spec_sub: forall x y, [sub x y] = [x] - [y]. + + Parameter opp : t -> t. + + Parameter spec_opp: forall x, [opp x] = - [x]. + + Parameter mul : t -> t -> t. + + Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. + + Parameter square : t -> t. + + Parameter spec_square: forall x, [square x] = [x] * [x]. + + Parameter power_pos : t -> positive -> t. + + Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. + + Parameter sqrt : t -> t. + + Parameter spec_sqrt: forall x, 0 <= [x] -> + [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + + Parameter div_eucl : t -> t -> t * t. + + Parameter spec_div_eucl: forall x y, [y] <> 0 -> + let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. + + Parameter div : t -> t -> t. + + Parameter spec_div: forall x y, [y] <> 0 -> [div x y] = [x] / [y]. + + Parameter modulo : t -> t -> t. + + Parameter spec_modulo: forall x y, [y] <> 0 -> + [modulo x y] = [x] mod [y]. + + Parameter gcd : t -> t -> t. + + Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). + +End ZType. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v new file mode 100644 index 0000000000..3d9d3d1901 --- /dev/null +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -0,0 +1,306 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id$ i*) + +Require Import ZArith. +Require Import ZAxioms. +Require Import ZSig. + +(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *) + +Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig. + +Delimit Scope IntScope with Int. +Bind Scope IntScope with Z.t. +Open Local Scope IntScope. +Notation "[ x ]" := (Z.to_Z x) : IntScope. +Infix "==" := Z.eq (at level 70) : IntScope. +Notation "0" := Z.zero : IntScope. +Infix "+" := Z.add : IntScope. +Infix "-" := Z.sub : IntScope. +Infix "*" := Z.mul : IntScope. +Notation "- x" := (Z.opp x) : IntScope. + +Hint Rewrite + Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ + Z.spec_mul Z.spec_opp Z.spec_of_Z : Zspec. + +Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec. + +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := Z.t. +Definition NZeq := Z.eq. +Definition NZ0 := Z.zero. +Definition NZsucc := Z.succ. +Definition NZpred := Z.pred. +Definition NZplus := Z.add. +Definition NZminus := Z.sub. +Definition NZtimes := Z.mul. + +Theorem NZeq_equiv : equiv Z.t Z.eq. +Proof. +repeat split; repeat red; intros; auto; congruence. +Qed. + +Add Relation Z.t Z.eq + reflexivity proved by (proj1 NZeq_equiv) + symmetry proved by (proj2 (proj2 NZeq_equiv)) + transitivity proved by (proj1 (proj2 NZeq_equiv)) + as NZeq_rel. + +Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Add Morphism NZpred with signature Z.eq ==> Z.eq as NZpred_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Add Morphism NZplus with signature Z.eq ==> Z.eq ==> Z.eq as NZplus_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Add Morphism NZminus with signature Z.eq ==> Z.eq ==> Z.eq as NZminus_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Add Morphism NZtimes with signature Z.eq ==> Z.eq ==> Z.eq as NZtimes_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Section Induction. + +Variable A : Z.t -> Prop. +Hypothesis A_wd : predicate_wd Z.eq A. +Hypothesis A0 : A 0. +Hypothesis AS : forall n, A n <-> A (Z.succ n). + +Add Morphism A with signature Z.eq ==> iff as A_morph. +Proof. apply A_wd. Qed. + +Let B (z : Z) := A (Z.of_Z z). + +Lemma B0 : B 0. +Proof. +unfold B; simpl. +rewrite <- (A_wd 0); auto. +zsimpl; auto. +Qed. + +Lemma BS : forall z : Z, B z -> B (z + 1). +Proof. +intros z H. +unfold B in *. apply -> AS in H. +setoid_replace (Z.of_Z (z + 1)) with (Z.succ (Z.of_Z z)); auto. +zsimpl; auto. +Qed. + +Lemma BP : forall z : Z, B z -> B (z - 1). +Proof. +intros z H. +unfold B in *. rewrite AS. +setoid_replace (Z.succ (Z.of_Z (z - 1))) with (Z.of_Z z); auto. +zsimpl; auto with zarith. +Qed. + +Lemma B_holds : forall z : Z, B z. +Proof. +intros; destruct (Z_lt_le_dec 0 z). +apply natlike_ind; auto with zarith. +apply B0. +intros; apply BS; auto. +replace z with (-(-z))%Z in * by (auto with zarith). +remember (-z)%Z as z'. +pattern z'; apply natlike_ind. +apply B0. +intros; rewrite Zopp_succ; unfold Zpred; apply BP; auto. +subst z'; auto with zarith. +Qed. + +Theorem NZinduction : forall n, A n. +Proof. +intro n. setoid_replace n with (Z.of_Z (Z.to_Z n)). +apply B_holds. +zsimpl; auto. +Qed. + +End Induction. + +Theorem NZplus_0_l : forall n, 0 + n == n. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZplus_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m). +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZminus_0_r : forall n, n - 0 == n. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZminus_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m). +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZtimes_0_l : forall n, 0 * n == 0. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZtimes_succ_l : forall n m, (Z.succ n) * m == n * m + m. +Proof. +intros; zsimpl; ring. +Qed. + +End NZAxiomsMod. + +Definition NZlt := Z.lt. +Definition NZle := Z.le. +Definition NZmin := Z.min. +Definition NZmax := Z.max. + +Infix "<=" := Z.le : IntScope. +Infix "<" := Z.lt : IntScope. + +Lemma spec_compare_alt : forall x y, Z.compare x y = ([x] ?= [y])%Z. +Proof. + intros; generalize (Z.spec_compare x y). + destruct (Z.compare x y); auto. + intros H; rewrite H; symmetry; apply Zcompare_refl. +Qed. + +Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z. +Proof. + intros; unfold Z.lt, Zlt; rewrite spec_compare_alt; intuition. +Qed. + +Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z. +Proof. + intros; unfold Z.le, Zle; rewrite spec_compare_alt; intuition. +Qed. + +Lemma spec_min : forall x y, [Z.min x y] = Zmin [x] [y]. +Proof. + intros; unfold Z.min, Zmin. + rewrite spec_compare_alt; destruct Zcompare; auto. +Qed. + +Lemma spec_max : forall x y, [Z.max x y] = Zmax [x] [y]. +Proof. + intros; unfold Z.max, Zmax. + rewrite spec_compare_alt; destruct Zcompare; auto. +Qed. + +Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd. +Proof. +intros x x' Hx y y' Hy. +rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd. +Proof. +intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism Z.le with signature Z.eq ==> Z.eq ==> iff as NZle_wd. +Proof. +intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism Z.min with signature Z.eq ==> Z.eq ==> Z.eq as NZmin_wd. +Proof. +intros; red; rewrite 2 spec_min; congruence. +Qed. + +Add Morphism Z.max with signature Z.eq ==> Z.eq ==> Z.eq as NZmax_wd. +Proof. +intros; red; rewrite 2 spec_max; congruence. +Qed. + +Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. +Proof. +intros. +unfold Z.eq; rewrite spec_lt, spec_le; omega. +Qed. + +Theorem NZlt_irrefl : forall n, ~ n < n. +Proof. +intros; rewrite spec_lt; auto with zarith. +Qed. + +Theorem NZlt_succ_r : forall n m, n < (Z.succ m) <-> n <= m. +Proof. +intros; rewrite spec_lt, spec_le, Z.spec_succ; omega. +Qed. + +Theorem NZmin_l : forall n m, n <= m -> Z.min n m == n. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_min. +generalize (Zmin_spec [n] [m]); omega. +Qed. + +Theorem NZmin_r : forall n m, m <= n -> Z.min n m == m. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_min. +generalize (Zmin_spec [n] [m]); omega. +Qed. + +Theorem NZmax_l : forall n m, m <= n -> Z.max n m == n. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_max. +generalize (Zmax_spec [n] [m]); omega. +Qed. + +Theorem NZmax_r : forall n m, n <= m -> Z.max n m == m. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_max. +generalize (Zmax_spec [n] [m]); omega. +Qed. + +End NZOrdAxiomsMod. + +Definition Zopp := Z.opp. + +Add Morphism Z.opp with signature Z.eq ==> Z.eq as Zopp_wd. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n. +Proof. +red; intros; zsimpl; auto with zarith. +Qed. + +Theorem Zopp_0 : - 0 == 0. +Proof. +red; intros; zsimpl; auto with zarith. +Qed. + +Theorem Zopp_succ : forall n, - (Z.succ n) == Z.pred (- n). +Proof. +intros; zsimpl; auto with zarith. +Qed. + +End ZSig_ZAxioms. |