From 3b4ffb3ed851458980267791273655b8512bf015 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 23 Jul 2024 22:08:52 +0900
Subject: [PATCH] dual variants

---
 CHANGELOG_UNRELEASED.md       |  1 +
 theories/constructive_ereal.v | 12 ++++++++++++
 2 files changed, 13 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index e89889d77..a7100e8db 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -41,6 +41,7 @@
 
 - in `constructive_ereal.v`:
   + lemmas `lteD2rE`, `leeD2rE`
+  + lemmas `lte_dadd2rE`, `lee_dadd2lE`
 
 ### Changed
 
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index 3a2b00dc7..0b2c5abeb 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -2764,6 +2764,18 @@ Proof. by rewrite daddeC; exact: gte_daddl. Qed.
 Lemma lte_dadd2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b).
 Proof. by move=> ?; rewrite !dual_addeE lteN2 lteD2lE ?fin_numN// lteN2. Qed.
 
+Lemma lte_dadd2rE x a b : x \is a fin_num -> (a + x < b + x) = (a < b).
+Proof.
+move=> ?; rewrite !dual_addeE lteN2 -[RHS]lteN2.
+by rewrite -[RHS](@lteD2rE _ (- x))// fin_numN.
+Qed.
+
+Lemma lee_dadd2rE x a b : x \is a fin_num -> (a + x <= b + x) = (a <= b).
+Proof.
+move=> ?; rewrite !dual_addeE leeN2 -[RHS]leeN2.
+by rewrite -[RHS](@leeD2rE _ (- x))// fin_numN.
+Qed.
+
 Lemma lee_dadd2l x a b : a <= b -> x + a <= x + b.
 Proof. rewrite !dual_addeE leeN2 -leeN2; exact: leeD2l. Qed.