diff options
| -rw-r--r-- | theories/Arith/Lt.v | 5 |
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. |