diff options
Diffstat (limited to 'theories/ZArith/Znat.v')
| -rw-r--r-- | theories/ZArith/Znat.v | 40 |
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. |