missing lemmas discovered while developing mathcomp-analysis

3 files changed, 13 insertions, 0 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index a1f334c..7a03f8e 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -11,6 +11,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 ### Added
 
 - Added contrapostion lemmas involving propositions: `contra_not`, `contraPnot`, `contraTnot`, `contraNnot`, `contraPT`, `contra_notT`, `contra_notN`, `contraPN`, `contraFnot`, `contraPF` and `contra_notF` in ssrbool.v and `contraPeq`, `contra_not_eq`, `contraPneq`, and `contra_neq_not` in eqtype.v
+- in `ssralg.v`, new lemma `sumr_const_nat` and `iter_addr_0`
+- in `ssrnum.v`, new lemma `ler_sum_nat`
 
 - in `seq.v`, new lemmas: `take_uniq`, `drop_uniq`
 - in `fintype.v`, new lemmas: `card_geqP`, `card_gt1P`, `card_gt2P`,
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 2bde8dd..9a3c7d7 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -835,6 +835,9 @@ Qed.
 Lemma mulrnAC x m n : x *+ m *+ n = x *+ n *+ m.
 Proof. by rewrite -!mulrnA mulnC. Qed.
 
+Lemma iter_addr_0 n (m : V) : iter n (+%R m) 0 = m *+ n.
+Proof. by elim: n => //= n ->; rewrite mulrS. Qed.
+
 Lemma sumrN I r P (F : I -> V) :
   (\sum_(i <- r | P i) - F i = - (\sum_(i <- r | P i) F i)).
 Proof. by rewrite (big_morph _ opprD oppr0). Qed.
@@ -856,6 +859,9 @@ Lemma sumr_const (I : finType) (A : pred I) (x : V) :
   \sum_(i in A) x = x *+ #|A|.
 Proof. by rewrite big_const -iteropE. Qed.
 
+Lemma sumr_const_nat (m n : nat) (x : V) : \sum_(n <= i < m) x = x *+ (m - n).
+Proof. by rewrite big_const_nat iter_addr_0. Qed.
+
 Lemma telescope_sumr n m (f : nat -> V) : n <= m ->
   \sum_(n <= k < m) (f k.+1 - f k) = f m - f n.
 Proof.
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 6198b44..45cd336 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -2016,6 +2016,11 @@ Lemma ler_sum I (r : seq I) (P : pred I) (F G : I -> R) :
   \sum_(i <- r | P i) F i <= \sum_(i <- r | P i) G i.
 Proof. exact: (big_ind2 _ (lexx _) ler_add). Qed.
 
+Lemma ler_sum_nat (m n : nat) (F G : nat -> R) :
+  (forall i, (m <= i < n)%N -> F i <= G i) ->
+  \sum_(m <= i < n) F i <= \sum_(m <= i < n) G i.
+Proof. by move=> le_FG; rewrite !big_nat ler_sum. Qed.
+
 Lemma psumr_eq0 (I : eqType) (r : seq I) (P : pred I) (F : I -> R) :
     (forall i, P i -> 0 <= F i) ->
   (\sum_(i <- r | P i) (F i) == 0) = (all (fun i => (P i) ==> (F i == 0)) r).