diff options
| -rw-r--r-- | theories/ZArith/Wf_Z.v | 7 | ||||
| -rw-r--r-- | theories/ZArith/Zorder.v | 7 |
2 files changed, 7 insertions, 7 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 4d11f92b04..f26caca8e8 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -96,13 +96,6 @@ Intros Hn; Elim Hn; Intros. Rewrite -> p; Apply H. Qed. -Lemma ZERO_le_inj : - (n:nat) `0 <= (inject_nat n)`. -Induction n; Simpl; Intros; -[ Apply Zle_n -| Unfold Zle; Simpl; Discriminate]. -Qed. - Lemma natlike_ind : (P:Z->Prop) (P `0`) -> ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) -> (x:Z) `0 <= x` -> (P x). diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 88da01bac7..bfe56b82e5 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -637,6 +637,13 @@ Lemma NEG_lt_ZERO : (p:positive)`(NEG p)<0`. Unfold Zlt; Trivial. Qed. +Lemma ZERO_le_inj : + (n:nat) `0 <= (inject_nat n)`. +Induction n; Simpl; Intros; +[ Apply Zle_n +| Unfold Zle; Simpl; Discriminate]. +Qed. + Hints Immediate Zle_refl : zarith. (** Transitivity using successor *) |