SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMax

 To retrieve the old behavior of spec_sub0 and spec_sub with
 precondition on order, just chain spec_sub with Zmax_r or Zmax_l.
 Idem with spec_pred0 and spec_pred.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12490 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 4 deletions

diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 5295aaec2..2dfa783aa 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -69,13 +69,11 @@ Module Type NType.
 
  Parameter pred : t -> t.
 
- Parameter spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.
- Parameter spec_pred0: forall x, [x] = 0 -> [pred x] = 0.
+ Parameter spec_pred: forall x, [pred x] = Zmax 0 ([x] - 1).
 
  Parameter sub : t -> t -> t.
 
- Parameter spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y].
- Parameter spec_sub0: forall x y, [x] < [y]-> [sub x y] = 0.
+ Parameter spec_sub: forall x y, [sub x y] = Zmax 0 ([x] - [y]).
 
  Parameter mul : t -> t -> t.