missing lemmas about ereal (#1264)

* missing lemmas about ereal * dual variants * renamings * minor generalization --------- Co-authored-by: Pierre Roux <[email protected]>
math-comp · Jul 25, 2024 · 899c141 · 899c141
1 parent b3cb11a
commit 899c141
Show file tree

Hide file tree

Showing 4 changed files with 179 additions and 61 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -39,6 +39,10 @@
 - in `realfun.v`:
   + lemma `nondecreasing_at_left_is_cvgr`
 
+- in `constructive_ereal.v`:
+  + lemmas `lteD2rE`, `leeD2rE`
+  + lemmas `lte_dD2rE`, `lee_dD2rE`
+
 ### Changed
 
 - in `topology.v`:
@@ -87,15 +91,53 @@
 - in `measure.v`:
   + `setD_closed` -> `setSD_closed`
 
+- in `constructive_ereal.v`:
+  + `lte_dadd` -> `lte_dD`
+  + `lee_daddl` -> `lee_dDl`
+  + `lee_daddr` -> `lee_dDr`
+  + `gee_daddl` -> `gee_dDl`
+  + `gee_daddr` -> `gee_dDr`
+  + `lte_daddl` -> `lte_dDl`
+  + `lte_daddr` -> `lte_dDr`
+  + `gte_dsubl` -> `gte_dBl`
+  + `gte_dsubr` -> `gte_dBr`
+  + `gte_daddl` -> `gte_dDl`
+  + `gte_daddr` -> `gte_dDr`
+  + `lee_dadd2lE` -> `lee_dD2lE`
+  + `lte_dadd2lE` -> `lte_dD2lE`
+  + `lee_dadd2rE` -> `lee_dD2rE`
+  + `lee_dadd2l` -> `lee_dD2l`
+  + `lee_dadd2r` -> `lee_dD2r`
+  + `lee_dadd` -> `lee_dD`
+  + `lee_dsub` -> `lee_dB`
+  + `lte_dsubl_addr` -> `lte_dBlDr`
+  + `lte_dsubl_addl` -> `lte_dBlDl`
+  + `lte_dsubr_addr` -> `lte_dBrDr`
+  + `lte_dsubr_addl` -> `lte_dBrDl`
+  + `gte_opp` -> `gteN`
+  + `gte_dopp` -> `gte_dN`
+  + `lte_le_add` -> `lte_leD`
+  + `lee_lt_add` -> `lee_ltD`
+  + `lte_le_dadd` -> `lte_le_dD`
+  + `lee_lt_dadd` -> `lee_lt_dD`
+  + `lte_le_sub` -> `lte_leB`
+  + `lte_le_dsub` -> `lte_le_dB`
+
 ### Generalized
 
+- in `constructive_ereal.v`:
+  + lemmas `leeN2`, `lteN2` generalized from `realDomainType` to `numDomainType`
+
 ### Deprecated
 
 - in `reals.v`:
   + `floor_le` (use `ge_floor` instead)
   + `le_floor` (use `Num.Theory.floor_le` instead)
   + `le_ceil` (use `ceil_ge` instead)
 
+- in `constructive_ereal.v`:
+  + lemmas `lte_opp2`, `lee_opp2` (use `lteN2`, `leeN2` instead)
+
 ### Removed
 
 - in `reals.v`: