diff options
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 3aec6ec3a7..e12d2f2ba1 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). |