diff options
| author | fredokun | 2017-11-29 17:22:45 +0100 |
|---|---|---|
| committer | fredokun | 2017-12-01 13:38:09 +0100 |
| commit | a6f0f03dcf002921f9f1b42a65bc023c4f6f4a84 (patch) | |
| tree | 9b87e4c1ec87641b842237d5bb1369004839afe6 | |
| parent | b23df225c7df7883af6ecfa921986cfb6fd3cd7c (diff) | |
proposed fix for issue #3213: extra variable m in Lt.S_pred
| -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 035c4e466d..2c2bea4a65 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. |