dual variants

math-comp · Jul 23, 2024 · 3b4ffb3 · 3b4ffb3
1 parent b60f80b
commit 3b4ffb3
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git 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
@@ -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.