diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-13 22:21:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-13 22:21:42 +0000 |
| commit | a9cce3d67a921065058274cf9f81bac25cf721c0 (patch) | |
| tree | d67717253050b7ff1609ba3b3a1b777e9f2fd123 /theories/Arith/Le.v | |
| parent | 90eea6b18bd76e840a5bf364230049700575d042 (diff) | |
Nouveaux lemmes (sur proposition de Nijmegen)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4010 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Le.v')
| -rwxr-xr-x | theories/Arith/Le.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 3aec6ec3a..e12d2f2ba 100755 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -60,6 +60,13 @@ Elim H ; Simpl ; Auto with arith. Qed. Hints Immediate le_S_n : arith v62. +Lemma le_pred : (n,m:nat)(le n m)->(le (pred n) (pred m)). +Proof. +Induction n. Simpl. Auto with arith. +Intros n0 Hn0. Induction m. Simpl. Intro H. Inversion H. +Intros n1 H H0. Simpl. Auto with arith. +Qed. + (** Negative properties *) Theorem le_Sn_O : (n:nat)~(le (S n) O). |