changelog

math-comp · Nov 15, 2024 · 56dbde7 · 56dbde7
1 parent 687806c
commit 56dbde7
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,9 @@
 
 ### Added
 
+- in file `mathcomp_extra.v`,
+  + lemmas `eq_lt_total`, `le_lt_total`
+
 - file `Rstruct_topology.v`
 
 - package `coq-mathcomp-reals` depending on `coq-mathcomp-classical`
@@ -182,6 +185,14 @@
 	* definition `mfun`
     * lemmas `mfun_rect`, `mfun_valP`, `mfuneqP`
 
+- in `sequences.v`,
+  + generalized indexing from zero-based ones (`0 <= k < n` and `k <oo`)
+    to `m <= k < n` and `m <= k <oo`
+    * lemmas `nondecreasing_series`, `ereal_nondecreasing_series`,
+             `eseries_mkcondl`, `eseries_mkcondr`, `eq_eseriesl`,
+	     `nneseries_lim_ge`, `adde_def_nneseries`,
+	     `nneseriesD`, `nneseries_sum_nat`, `nneseries_sum`
+
 ### Deprecated
 
 - in `topology_structure.v`:

diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
@@ -547,4 +547,3 @@ Proof. by case/boolP: (x == y)=> // ?; apply/orP; right; exact:lt_total. Qed.
 Lemma le_lt_total {disp : unit} {T : orderType disp} (x y : T) :
   (x <= y)%O || (y < x)%O.
 Proof. by rewrite le_eqVlt -orbA eq_lt_total. Qed.
-
Original file line number	Diff line number	Diff line change
Expand Up		@@ -547,4 +547,3 @@ Proof. by case/boolP: (x == y)=> // ?; apply/orP; right; exact:lt_total. Qed.
		Lemma le_lt_total {disp : unit} {T : orderType disp} (x y : T) :
		(x <= y)%O \|\| (y < x)%O.
		Proof. by rewrite le_eqVlt -orbA eq_lt_total. Qed.