diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-18 10:40:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-18 10:40:05 +0000 |
| commit | 8dbc29de13c5cb91bff356d7c729f0d30d6b46ad (patch) | |
| tree | 51dd37abe10cc14664833850c8f25735f297512d /theories/ZArith | |
| parent | c089377ca84a88401e83e747eefeb0a608c8a33b (diff) | |
Deplacement ZERO_le_inj dans Zorder
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4933 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
| -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 4d11f92b0..f26caca8e 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 88da01bac..bfe56b82e 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 *) |