cleanup of Zsgn

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

1 files changed, 40 insertions, 0 deletions

diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index bc3d73484..84262469b 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -290,6 +290,16 @@ Proof.
  intros Hn Hm. now rewrite <- N2Z.inj_compare, !id.
 Qed.
 
+Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.to_N n <= Z.to_N m)%N).
+Proof.
+ intros Hn Hm. unfold Z.le, N.le. now rewrite inj_compare.
+Qed.
+
+Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.to_N n < Z.to_N m)%N).
+Proof.
+ intros Hn Hm. unfold Z.lt, N.lt. now rewrite inj_compare.
+Qed.
+
 Lemma inj_min n m : Z.to_N (Z.min n m) = N.min (Z.to_N n) (Z.to_N m).
 Proof.
  destruct n, m; simpl; trivial; unfold Z.min, N.min; simpl;
@@ -386,6 +396,16 @@ Proof.
  intros. rewrite !abs_N_nonneg by trivial. now apply Z2N.inj_compare.
 Qed.
 
+Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.abs_N n <= Z.abs_N m)%N).
+Proof.
+ intros Hn Hm. unfold Z.le, N.le. now rewrite inj_compare.
+Qed.
+
+Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.abs_N n < Z.abs_N m)%N).
+Proof.
+ intros Hn Hm. unfold Z.lt, N.lt. now rewrite inj_compare.
+Qed.
+
 Lemma inj_min n m : 0<=n -> 0<=m ->
  Z.abs_N (Z.min n m) = N.min (Z.abs_N n) (Z.abs_N m).
 Proof.
@@ -619,6 +639,16 @@ Proof.
  intros Hn Hm. now rewrite <- Nat2Z.inj_compare, !id.
 Qed.
 
+Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.to_nat n <= Z.to_nat m)%nat).
+Proof.
+ intros Hn Hm. unfold Z.le. now rewrite nat_compare_le, inj_compare.
+Qed.
+
+Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.to_nat n < Z.to_nat m)%nat).
+Proof.
+ intros Hn Hm. unfold Z.lt. now rewrite nat_compare_lt, inj_compare.
+Qed.
+
 Lemma inj_min n m : Z.to_nat (Z.min n m) = min (Z.to_nat n) (Z.to_nat m).
 Proof.
  now rewrite <- !Z_N_nat, Z2N.inj_min, N2Nat.inj_min.
@@ -708,6 +738,16 @@ Proof.
  intros. now rewrite <- !Zabs_N_nat, <- N2Nat.inj_compare, Zabs2N.inj_compare.
 Qed.
 
+Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.abs_nat n <= Z.abs_nat m)%nat).
+Proof.
+ intros Hn Hm. unfold Z.le. now rewrite nat_compare_le, inj_compare.
+Qed.
+
+Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.abs_nat n < Z.abs_nat m)%nat).
+Proof.
+ intros Hn Hm. unfold Z.lt. now rewrite nat_compare_lt, inj_compare.
+Qed.
+
 Lemma inj_min n m : 0<=n -> 0<=m ->
  Z.abs_nat (Z.min n m) = min (Z.abs_nat n) (Z.abs_nat m).
 Proof.