Dual ereal

CHANGELOG_UNRELEASED.md

@@ -105,6 +105,31 @@
     `le0_muleDl`, `le0_muleDr`, `le0_sume_distrl`, `le0_sume_distrr`,
     `adde_defNN`, `minEFin`, `mine_ninftyl`, `mine_ninftyr`, `mine_pinftyl`,
     `mine_pinftyr`, `oppe_max`, `oppe_min`, `mineMr`, `mineMl`
+  + definitions `dual_adde`
+  + notations for the above in scope `ereal_dual_scope` delimited by `dE`
+  + lemmas `dual_addeE`, `dual_sumeE`, `dual_addeE_def`, `daddEFin`,
+    `dsumEFin`, `dsubEFin`, `dadde0`, `dadd0e`, `daddeC`, `daddeA`,
+    `daddeAC`, `daddeCA`, `daddeACA`, `doppeD`, `dsube0`, `dsub0e`, `daddeK`,
+    `dfin_numD`, `dreal_of_extendedD`, `dsubeK`, `dsube_eq`,
+    `dsubee`, `dadde_eq_pinfty`, `daddooe`, `dadde_Neq_pinfty`,
+    `dadde_Neq_ninfty`, `desum_fset_pinfty`, `desum_pinfty`,
+    `desum_fset_ninfty`, `desum_ninfty`, `dadde_ge0`, `dadde_le0`,
+    `dsume_ge0`, `dsume_le0`, `dsube_lt0`, `dsubre_le0`,
+    `dsuber_le0`, `dsube_ge0`, `lte_dadd`, `lee_daddl`, `lee_daddr`,
+    `gee_daddl`, `gee_daddr`, `lte_daddl`, `lte_daddr`, `gte_dsubl`,
+    `gte_dsubr`, `lte_dadd2lE`, `lee_dadd2l`, `lee_dadd2lE`,
+    `lee_dadd2r`, `lee_dadd`, `lte_le_dadd`, `lee_dsub`,
+    `lte_le_dsub`, `lee_dsum`, `lee_dsum_nneg_subset`,
+    `lee_dsum_npos_subset`, `lee_dsum_nneg`, `lee_dsum_npos`,
+    `lee_dsum_nneg_ord`, `lee_dsum_npos_ord`, `lee_dsum_nneg_natr`,
+    `lee_dsum_npos_natr`, `lee_dsum_nneg_natl`, `lee_dsum_npos_natl`,
+    `lee_dsum_nneg_subfset`, `lee_dsum_npos_subfset`,
+    `lte_dsubl_addr`, `lte_dsubl_addl`, `lte_dsubr_addr`,
+    `lee_dsubr_addr`, `lee_dsubl_addr`, `ge0_dsume_distrl`, `dmulrEDr`,
+    `dmulrEDl`, `dge0_mulreDr`, `dge0_mulreDl`, `dle0_mulreDr`, `dle0_mulreDl`,
+    `ge0_dsume_distrr`, `le0_dsume_distrl`, `le0_dsume_distrr`,
+    `lee_abs_dadd`, `lee_abs_dsum`, `lee_abs_dsub`, `dadde_minl`, `dadde_minr`,
+    `lee_dadde`, `lte_spdaddr`
 - in `normedtype.v`:
   + lemma `mule_continuous`
 - in `cardinality.v`: