aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--theories/Arith/Lt.v5
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 035c4e466..2c2bea4a6 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -107,6 +107,11 @@ Proof.
intros. symmetry. now apply Nat.lt_succ_pred with m.
Qed.
+Lemma S_pred_pos n: O < n -> n = S (pred n).
+Proof.
+ apply S_pred.
+Qed.
+
Lemma lt_pred n m : S n < m -> n < pred m.
Proof.
apply Nat.lt_succ_lt_pred.