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/Zorder.v | |
| 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/Zorder.v')
| -rw-r--r-- | theories/ZArith/Zorder.v | 7 |
1 files changed, 7 insertions, 0 deletions
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 *) |