From f27c0d80d70993840cb4c17a6522be1f4e05d6ca Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Sat, 23 Aug 2025 11:36:19 +0200
Subject: [PATCH] littleoE0

Co-authored-by mkerjean
---
 CHANGELOG_UNRELEASED.md | 2 ++
 theories/landau.v       | 5 +++++
 2 files changed, 7 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index cb9c201927..e210adec3e 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -33,6 +33,8 @@
   + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope`
 - in `pseudometric_normed_Zmodule.v`:
   + lemma `le0_ball0`
+- in `theories/landau.v`:
+  + lemma `littleoE0`
 
 ### Changed
 
diff --git a/theories/landau.v b/theories/landau.v
index 4e0ad17b92..1be397623a 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -390,6 +390,11 @@ Lemma littleoE (tag : unit) (F : filter_on T)
    littleo_def F f h -> the_littleo tag F phF f h = f.
 Proof. by move=> /asboolP?; rewrite /the_littleo /insubd insubT. Qed.
 
+Lemma littleoE0 (tag : unit) (F : filter_on T)
+   (phF : phantom (set (set T)) F) f h :
+   ~ littleo_def F f h -> the_littleo tag F phF f h = 0.
+Proof. by move=> ?; rewrite /the_littleo /insubd insubN//; apply/asboolP. Qed.
+
 Canonical the_littleo_littleo (tag : unit) (F : filter_on T)
   (phF : phantom (set_system T) F) f h := [littleo of the_littleo tag F phF f h].