From 5f44633d0a46d43d94a7bcb61135176c5f5c569a Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Tue, 18 Jul 2023 23:53:46 +0900
Subject: [PATCH] fixes #979 (#980)

---
 CHANGELOG_UNRELEASED.md | 3 +++
 theories/topology.v     | 9 ++++-----
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 351179250..0252e99cf 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -162,6 +162,9 @@
 
 ### Removed
 
+- in `topology.v`:
+  + lemma `my_ball_le` (use `ball_le` instead)
+
 ### Infrastructure
 
 ### Misc
diff --git a/theories/topology.v b/theories/topology.v
index 61b09c7e1..29d6f29f8 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -4902,13 +4902,12 @@ Export PseudoMetric.Exports.
 
 Section PseudoMetricUniformity.
 
-Lemma my_ball_le (R : numDomainType) (M : Type) (ent : set (set (M * M)))
+Let ball_le (R : numDomainType) (M : Type) (ent : set (set (M * M)))
     (m : PseudoMetric.mixin_of R ent) :
   forall (x : M), {homo PseudoMetric.ball m x : e1 e2 / e1 <= e2 >-> e1 `<=` e2}.
 Proof.
-move=> x e1 e2 le12 y xe1_y.
-move: le12; rewrite le_eqVlt => /orP [/eqP <- //|].
-rewrite -subr_gt0 => lt12.
+move=> x e1 e2 + y xe1_y.
+rewrite le_eqVlt => /predU1P[<- //|]; rewrite -subr_gt0 => lt12.
 rewrite -[e2](subrK e1); apply: PseudoMetric.ball_triangle xe1_y.
 suff : PseudoMetric.ball m x (PosNum lt12)%:num x by [].
 exact: PseudoMetric.ball_center.
@@ -4922,7 +4921,7 @@ Next Obligation.
 move=> R T ent nbhs nbhsE m; rewrite (PseudoMetric.entourageE m).
 apply: filter_from_filter; first by exists 1 => /=.
 move=> _ _ /posnumP[e1] /posnumP[e2]; exists (Num.min e1 e2)%:num => //=.
-by rewrite subsetI; split=> ?; apply: my_ball_le;
+by rewrite subsetI; split=> ?; apply: ball_le;
    rewrite -leEsub// le_minl lexx ?orbT.
 Qed.
 Next Obligation.