From 573b92158382692ec60c7cc7059f76987603dd86 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 19 Jul 2024 11:25:35 +0900
Subject: [PATCH] `at_left` version of an `at_right` lemma (#1255)

* at_left version of an at_right lemma
---
 CHANGELOG_UNRELEASED.md |  3 +++
 theories/realfun.v      | 17 ++++++++++++++++-
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 272348558..6fecd383e 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -36,6 +36,9 @@
 - in `mathcomp_extra.v`:
   + lemmas `intr1D`, `intrD1`, `floor_eq`, `floorN`
 
+- in `realfun.v`:
+  + lemma `nondecreasing_at_left_is_cvgr`
+
 ### Changed
 
 - in `topology.v`:
diff --git a/theories/realfun.v b/theories/realfun.v
index 24735d797..8a5bdd953 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -365,9 +365,24 @@ by eexists; apply: (@nondecreasing_at_right_cvgr _ _ (BLeft b));
   [rewrite bnd_simp|near: b..].
 Unshelve. all: by end_near. Qed.
 
+Lemma nondecreasing_at_left_is_cvgr f a :
+    (\forall x \near a^'-, {in `]x, a[ &, {homo f : n m / n <= m}}) ->
+    (\forall x \near a^'-, has_ubound [set f y | y in `]x, a[]) ->
+  cvg (f x @[x --> a^'-]).
+Proof.
+move=> ndf ubf; suff: cvg ((f \o -%R) x @[x --> (- a)^'+]).
+  move=> /cvg_ex[/= l fal].
+  by apply/cvg_ex; exists l; exact/cvg_at_leftNP.
+apply: @nonincreasing_at_right_is_cvgr.
+- rewrite at_rightN near_simpl; apply: filterS ndf => x ndf y z.
+  by rewrite -2!oppr_itvoo => yxa zxa yz; rewrite ndf// lerNr opprK.
+- rewrite at_rightN near_simpl; apply: filterS ubf => x [r ubf].
+  exists r => _/= [s sax <-]; rewrite ubf//=; exists (- s) => //.
+  by rewrite oppr_itvoo.
+Qed.
+
 End fun_cvg_realType.
 Arguments nondecreasing_at_right_cvgr {R f a} b.
-Arguments nondecreasing_at_right_cvgr {R f a} b.
 
 Section fun_cvg_ereal.
 Context {R : realType}.