diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 6 |
2 files changed, 8 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1e779c3..839e796 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,6 +10,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Added +- in `ssrnat.v`, added lemma `sumnB`. + - in `seq.v`, + new higher-order predicate `pairwise r xs` which asserts that the relation `r` holds for any i-th and j-th element of `xs` such that i < j. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index c1f420f..5da7a91 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1907,6 +1907,12 @@ Lemma leq_sum I r (P : pred I) (E1 E2 : I -> nat) : \sum_(i <- r | P i) E1 i <= \sum_(i <- r | P i) E2 i. Proof. by move=> leE12; elim/big_ind2: _ => // m1 m2 n1 n2; apply: leq_add. Qed. +Lemma sumnB I r (P : pred I) (E1 E2 : I -> nat) : + (forall i, P i -> E1 i <= E2 i) -> + \sum_(i <- r | P i) (E2 i - E1 i) = + \sum_(i <- r | P i) E2 i - \sum_(i <- r | P i) E1 i. +Proof. by move=> /(_ _ _)/subnK-/(eq_bigr _)<-; rewrite big_split addnK. Qed. + Lemma sum_nat_eq0 (I : finType) (P : pred I) (E : I -> nat) : (\sum_(i | P i) E i == 0)%N = [forall (i | P i), E i == 0%N]. Proof. by rewrite eq_sym -(@leqif_sum I P _ (fun _ => 0%N) E) ?big1_eq. Qed. |