diff options
| author | Reynald Affeldt | 2021-01-19 01:36:20 +0900 |
|---|---|---|
| committer | Reynald Affeldt | 2021-01-19 01:36:20 +0900 |
| commit | e1d5e9c2585bad2e9c27a476276761cc71ff9c91 (patch) | |
| tree | d9c96475a5e055a665e006a8ce2f147d34aea271 | |
| parent | 35fc6b309a5cc87570255addfd135cb4650ebb43 (diff) | |
fixes #694
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/interval.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1e779c3..b2a4ad1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -22,7 +22,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v`, new lemmas: `sorted_pairwise(_in)`, `path_pairwise(_in)`, `cycle_all2rel(_in)`, `pairwise_sort`, and `sort_pairwise_stable`. -- in `interval.v`, new lemmas: `ge_pinftyE`, `le_ninftyE`, `gt_pinfty`, `lt_ninfty`. +- in `interval.v`, new lemmas: `ge_pinfty`, `le_ninfty`, `gt_pinfty`, `lt_ninfty`. ### Changed diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 4a1cadb..b6964f1 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -217,9 +217,9 @@ Proof. by rewrite /<=%O /= lteifxx. Qed. Lemma bound_ltxx c1 c2 x : (BSide c1 x < BSide c2 x) = (c1 && ~~ c2). Proof. by rewrite /<%O /= lteifxx. Qed. -Lemma ge_pinftyE b : (+oo <= b) = (b == +oo). Proof. by move: b => [|[]]. Qed. +Lemma ge_pinfty b : (+oo <= b) = (b == +oo). Proof. by move: b => [|[]]. Qed. -Lemma le_ninftyE b : (b <= -oo) = (b == -oo). Proof. by case: b => // - []. Qed. +Lemma le_ninfty b : (b <= -oo) = (b == -oo). Proof. by case: b => // - []. Qed. Lemma gt_pinfty b : (+oo < b) = false. Proof. by []. Qed. |