diff options
| author | Maxime Dénès | 2018-02-21 19:07:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-21 19:07:05 +0100 |
| commit | e97c27b468901aaea148ae775e070bad6eb42571 (patch) | |
| tree | 3d306f16a062e44ba2f7e7930c1fa8545c95e691 | |
| parent | cec85230d0a6c8c546d3297d6108917f7a3157e7 (diff) | |
| parent | a6f0f03dcf002921f9f1b42a65bc023c4f6f4a84 (diff) | |
Merge PR #6282: 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. |