fix changelog

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -6,37 +6,28 @@
 
 - in `probability.v`:
   + lemmas `eq_bernoulli`, `eq_bernoulliV2`
-- file `mathcomp_extra.v`
-  + lemmas `ge_trunc`, `lt_succ_trunc`, `trunc_ge_nat`, `trunc_lt_nat`
 
-- file `Rstruct.v`
-  + lemma `Pos_to_natE` (from `mathcomp_extra.v`)
-  + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE`
+- in `measure.v`:
+  + lemmas `mnormalize_id`, `measurable_fun_eqP`
 
-- new file `internal_Eqdep_dec.v` (don't use, internal, to be removed)
+- in `ftc.v`:
+  + lemma `integrable_locally`
 
-- file `constructive_ereal.v`:
-  + definition `iter_mule`
-  + lemma `prodEFin`
+- in `constructive_ereal.v`:
+  + lemma `EFin_bigmax`
 
-- file `exp.v`:
-  + lemma `expR_sum`
+- in `mathcomp_extra.v`:
+  + lemmas `inr_inj`, `inl_inj`
 
-- file `lebesgue_integral.v`:
-  + lemma `measurable_fun_le`
+- in `classical_sets.v`:
+  + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f`
+  + lemmas `inr_in_set_inl`, `inl_in_set_inl`
 
-- in `trigo.v`:
-  + lemma `integral0oo_atan`
+- in `lebesgue_integral_approximation.v`:
+  + lemma `measurable_prod`
 
 - in `measure.v`:
-  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_compS`
-  + lemma `preimage_set_system_id`
-
-- in `Rstruct_topology.v`:
-  + lemma `RexpE`
-
-- file `mathcomp_extra.v`:
-  + lemma `mulr_funEcomp`
+  + lemma `preimage_set_system_compS`
 
 - in `numfun.v`:
   + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-`
@@ -69,28 +60,6 @@
   + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`,
     ` expectation_mul`
 
-- in `trigo.v`:
-  + lemma `integral0oo_atan`
-
-- in `measure.v`:
-  + lemmas `mnormalize_id`, `measurable_fun_eqP`
-
-- in `ftc.v`:
-  + lemma `integrable_locally`
-
-- in `constructive_ereal.v`:
-  + lemma `EFin_bigmax`
-
-- in `mathcomp_extra.v`:
-  + lemmas `inr_inj`, `inl_inj`
-
-- in `classical_sets.v`:
-  + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f`
-  + lemmas `inr_in_set_inl`, `inl_in_set_inl`
-
-- in `lebesgue_integral_approximation.v`:
-  + lemma `measurable_prod`
-
 ### Changed
 
 - in `pi_irrational`:
@@ -104,50 +73,13 @@
   + `fubini1a` -> `integrable12ltyP`
   + `fubini1b` -> `integrable21ltyP`
   + `measurable_funP` -> `measurable_funPT` (field of `isMeasurableFun` mixin)
-
-- in `mathcomp_extra.v`
-  + `comparable_min_le_min` -> `comparable_le_min2`
-  + `comparable_max_le_max` -> `comparable_le_max2`
-  + `min_le_min` -> `le_min2`
-  + `max_le_max` -> `le_max2`
-  + `real_sqrtC` -> `sqrtC_real`
 
 ### Generalized
 
 ### Deprecated
 
 ### Removed
 
-- file `mathcomp_extra.v`
-  + lemma `Pos_to_natE` (moved to `Rstruct.v`)
-  + lemma `deg_le2_ge0` (available as `deg_le2_poly_ge0` in `ssrnum.v`
-    since MathComp 2.1.0)
-
-- in `lebesgue_integral.v`:
-  + definition `cst_mfun`
-  + lemma `mfun_cst`
-
-- in `cardinality.v`:
-  + lemma `cst_fimfun_subproof`
-
-- in `lebesgue_integral.v`:
-  + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
-  + lemma `cst_nnfun_subproof` (turned into a `Let`)
-  + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead)
-
-- in `lebesgue_integral.v`:
-  + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
-  + notation `measurable_fun_indic` (deprecation since 0.6.3)
-- in `constructive_ereal.v`
-  + notation `lee_opp` (deprecated since 0.6.5)
-  + notation `lte_opp` (deprecated since 0.6.5)
-- in `measure.v`:
-  + `dynkin_setI_bigsetI` (use `big_ind` instead)
-
-- in `lebesgue_measurable.v`:
-  + notation `measurable_fun_power_pos` (deprecated since 0.6.3)
-  + notation `measurable_power_pos` (deprecated since 0.6.4)
-
 ### Infrastructure
 
 ### Misc