diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 12:19:35 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 12:19:35 +0000 |
| commit | f0e24c6a8b66e86a22370fcc45d1f3e7543496fd (patch) | |
| tree | a31bdda34c4380c864e494f82b2a5e0dbb122a98 /theories/ZArith/Wf_Z.v | |
| parent | 450763ee0152a75881a8618172cc36bb6350ea9a (diff) | |
ground->firstorder, cc-> congruence, CC final commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Wf_Z.v')
| -rw-r--r-- | theories/ZArith/Wf_Z.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index f26caca8e..eecfc42b2 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -179,7 +179,7 @@ Apply Hrec; Intros. Assert H2: `0<0`. Apply Zle_lt_trans with y; Intuition. Inversion H2. -Ground. +Firstorder. Unfold Zle Zcompare in H; Elim H; Auto. Defined. |