Library Algebra.Monoid.Monoid_sum
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Support for the iteration of the commutative monoid law.
Let G be an AbelianMonoid.
Let u be an n-family of G.
Let G1 G2 : AbelianMonoid.
Let f : G1 → G2.
This module may be used through the import of Algebra.Monoid.Monoid,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- sum u is the iteration of plus for all items of u (from 0 to n-1);
- sum_part u i is the partial sum of items of u, from 0 to i-1.
- f_sum_compat f states that f transports the iterated monoid law sum.
Used logic axioms
- classic, the weak form of excluded middle.
Usage
From Requisite Require Import stdlib_wR.
From Requisite Require Import ssr_wMC.
From mathcomp Require Import bigop.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid_compl Monoid_FF.
Local Open Scope Monoid_scope.
Section Sum_Def.
Context {G : AbelianMonoid}.
Definition plus_m : Monoid.law (@zero G).
Proof.
∃ plus; repeat split; intro;
[apply plus_assoc | apply plus_zero_l | apply plus_zero_r].
Defined.
Definition plus_cm : Monoid.com_law (@zero G).
Proof.
∃ plus; repeat split; intro;
[apply plus_assoc | apply plus_zero_l | apply plus_zero_r |
apply plus_comm].
Defined.
Lemma plus_cm_correct : ∀ (u v : G), u + v = plus_cm u v.
Proof. easy. Qed.
Definition sum {n} (u : 'G^n) : G := \big[plus_cm/0]_(i < n) u i.
Lemma sum_eq : ∀ {n} (u v : 'G^n), u = v → sum u = sum v.
Proof. intros; subst; easy. Qed.
Lemma sum_ext :
∀ {n} (u v : 'G^n), (∀ i, u i = v i) → sum u = sum v.
Proof. move=>> /extF → //. Qed.
End Sum_Def.
Section Sum_Bigop_Wrapper.
Context {G : AbelianMonoid}.
Lemma sum_zero_compat :
∀ {n} (u : 'G^n), u = 0 → sum u = 0.
Proof. move=>> H; apply big1; rewrite H; easy. Qed.
Lemma sum_nil : ∀ (u : 'G^0), sum u = 0.
Proof. intros; apply big_ord0. Qed.
Lemma sum_ind_l : ∀ {n} (u : 'G^n.+1), sum u = u ord0 + sum (liftF_S u).
Proof. intros; apply big_ord_recl. Qed.
Lemma sum_ind_r :
∀ {n} (u : 'G^n.+1), sum u = sum (widenF_S u) + u ord_max.
Proof. intros; apply big_ord_recr. Qed.
Lemma sum_plus : ∀ {n} (u v : 'G^n), sum (u + v) = sum u + sum v.
Proof.
intros; rewrite 2!plus_cm_correct; unfold sum.
rewrite <- big_split; apply eq_bigr; easy.
Qed.
End Sum_Bigop_Wrapper.
Section Sum_Facts1.
Context {G : AbelianMonoid}.
Lemma sum_castF_compat :
∀ {n1 n2} (H : n1 = n2) (u1 : 'G^n1) (u2 : 'G^n2),
castF H u1 = u2 → sum u1 = sum u2.
Proof. intros; subst; apply sum_ext; intros; rewrite castF_id; easy. Qed.
Lemma sum_castF :
∀ {n1 n2} (H : n1 = n2) (u : 'G^n1),
sum (castF H u) = sum u.
Proof. intros; eapply eq_sym, (sum_castF_compat); easy. Qed.
Lemma sum_zero : ∀ {n}, sum (0 : 'G^n) = 0.
Proof. intros; apply sum_zero_compat; easy. Qed.
Lemma fct_sum_eq :
∀ {T : Type} {n} (f : '(T → G)^n) t, sum f t = sum (f^~ t).
Proof.
intros T n f t; induction n as [| n Hn]; try now rewrite 2!sum_nil.
rewrite 2!sum_ind_l fct_plus_eq Hn; easy.
Qed.
Lemma sum_nil' : ∀ {n} (u : 'G^n), n = 0 → sum u = 0.
Proof. intros; subst; apply sum_nil. Qed.
Lemma sum_1 : ∀ (u : 'G^1), sum u = u ord0.
Proof. intros; rewrite sum_ind_l sum_nil; apply plus_zero_r. Qed.
Lemma sum_1_alt : ∀ {n} (u : 'G^n.+1), n = 0 → sum u = u ord0.
Proof. intros; subst; apply sum_1. Qed.
Lemma sum_2 : ∀ (u : 'G^2), sum u = u ord0 + u ord_max.
Proof.
intros; rewrite sum_ind_l sum_1; f_equal.
rewrite -(I_1_is_unit ord_max) liftF_S_max; easy.
Qed.
Lemma sum_3 : ∀ (u : 'G^3), sum u = u ord0 + u ord1 + u ord_max.
Proof.
intros; rewrite sum_ind_l sum_2 plus_assoc; f_equal.
rewrite liftF_S_max; easy.
Qed.
Lemma sum_singleF : ∀ (u0 : G), sum (singleF u0) = u0.
Proof. intros; rewrite sum_1 singleF_0; easy. Qed.
Lemma sum_coupleF : ∀ (u0 u1 : G), sum (coupleF u0 u1) = u0 + u1.
Proof. intros; rewrite sum_2 coupleF_0 coupleF_1; easy. Qed.
Lemma sum_tripleF :
∀ (u0 u1 u2 : G), sum (tripleF u0 u1 u2) = u0 + u1 + u2.
Proof. intros; rewrite sum_3 tripleF_0 tripleF_1 tripleF_2; easy. Qed.
Lemma sum_concatF :
∀ {n1 n2} (u1 : 'G^n1) (u2 : 'G^n2),
sum (concatF u1 u2) = sum u1 + sum u2.
Proof.
intros n1 n2 u1 u2; induction n2 as [| n2 Hn2].
rewrite !concatF_nil_r sum_nil plus_zero_r; apply sum_castF.
rewrite -(sum_castF (addnS n1 n2)) !sum_ind_r plus_assoc -Hn2. do 2 f_equal.
apply widenF_S_concatF.
apply concatF_last.
Qed.
Lemma sum_concatF_zero_l :
∀ {n1 n2} (u2 : 'G^n2), sum (concatF (0 : 'G^n1) u2) = sum u2.
Proof. intros; rewrite sum_concatF sum_zero plus_zero_l; easy. Qed.
Lemma sum_concatF_zero_r :
∀ {n1 n2} (u1 : 'G^n1), sum (concatF u1 (0 : 'G^n2)) = sum u1.
Proof. intros; rewrite sum_concatF sum_zero plus_zero_r; easy. Qed.
Lemma sum_splitF :
∀ {n1 n2} (u : 'G^(n1 + n2)), sum u = sum (firstF u) + sum (lastF u).
Proof. intros n1 n2 u; rewrite {1}(concatF_splitF u); apply sum_concatF. Qed.
Lemma sum_skipF : ∀ {n} (u : 'G^n.+1) i0, sum u = u i0 + sum (skipF u i0).
Proof.
intros n u i0.
rewrite -(sum_castF (ordS_splitS i0)) sum_splitF sum_ind_r.
rewrite -(sum_castF (ord_split i0)) sum_splitF.
rewrite plus_assoc (plus_comm (u i0) _).
repeat f_equal.
rewrite firstF_skipF firstF_ord_splitS; easy.
apply firstF_ordS_splitS_last.
rewrite lastF_skipF; easy.
Qed.
Lemma sum_skipF_ex :
∀ {n} u0 (u1 : 'G^n) i0,
∃ u, sum u = u0 + sum u1 ∧ u i0 = u0 ∧ skipF u i0 = u1.
Proof.
intros n u0 u1 i0; destruct (skipF_ex u0 u1 i0) as [u [Hu0 Hu1]].
∃ u; repeat split; try easy; rewrite -Hu0 -Hu1; apply sum_skipF.
Qed.
Lemma sum_one : ∀ {n} (u : 'G^n.+1) i0, skipF u i0 = 0 → sum u = u i0.
Proof.
intros; erewrite sum_skipF, sum_zero_compat; try apply plus_zero_r; easy.
Qed.
Lemma sum_skip_zero :
∀ {n} (u : 'G^n.+1) i0, u i0 = 0 → sum u = sum (skipF u i0).
Proof.
move=>> Hi0; rewrite -(plus_zero_l (sum (skipF _ _))) -Hi0; apply sum_skipF.
Qed.
Lemma sum_skip2F :
∀ {n} (u : 'G^n.+2) {i0 i1} (H : i1 ≠ i0),
sum u = u i0 + u i1 + sum (skip2F u H).
Proof.
intros n u i0 i1 H.
rewrite (sum_skipF _ i0) -plus_assoc; f_equal.
rewrite (sum_skipF _ (insert_ord H)) skip2F_correct; f_equal.
rewrite skipF_correct; easy.
Qed.
Lemma sum_two :
∀ {n} (u : 'G^n.+2) {i0 i1 : 'I_n.+2} (H : (i1 ≠ i0)%nat),
skip2F u H = 0 → sum u = u i0 + u i1.
Proof.
move=>> H; erewrite sum_skip2F, sum_zero_compat. apply plus_zero_r. apply H.
Qed.
Lemma sum_insertF :
∀ {n} (u : 'G^n) x0 i0, sum (insertF u x0 i0) = x0 + sum u.
Proof.
intros; erewrite sum_skipF; rewrite → insertF_correct_l, skipF_insertF; easy.
Qed.
Lemma sum_insert2F :
∀ {n} (u : 'G^n) x0 x1 {i0 i1} (H : i1 ≠ i0),
sum (insert2F u x0 x1 H) = x0 + x1 + sum u.
Proof. intros; rewrite insert2F_correct 2!sum_insertF; apply plus_assoc. Qed.
Lemma sum_replaceF :
∀ {n} (u : 'G^n.+1) x0 i0, u i0 + sum (replaceF u x0 i0) = x0 + sum u.
Proof.
intros n u x0 i0; rewrite replaceF_equiv_def_insertF sum_insertF (sum_skipF u i0).
rewrite 2!plus_assoc (plus_comm (u i0)); easy.
Qed.
Lemma sum_replace2F :
∀ {n} (u : 'G^n.+2) x0 x1 {i0 i1},
i1 ≠ i0 → u i0 + u i1 + sum (replace2F u x0 x1 i0 i1) = x0 + x1 + sum u.
Proof.
intros n u x0 x1 i0 i1 H; unfold replace2F.
rewrite (plus_comm x0) -plus_assoc -(replaceF_correct_r _ x0 H).
rewrite sum_replaceF plus_comm3_l sum_replaceF plus_assoc; easy.
Qed.
Lemma sum_replace2F_eq :
∀ {n} (u : 'G^n.+2) x0 x1 {i0 i1},
i1 = i0 → u i1 + sum (replace2F u x0 x1 i0 i1) = x1 + sum u.
Proof. intros; rewrite → replace2F_correct_eq, sum_replaceF; easy. Qed.
Lemma sum_permutF :
∀ {n} p (u : 'G^n), injective p → sum (permutF p u) = sum u.
Proof.
intros n p u Hp; induction n as [| n].
rewrite !sum_nil; easy.
rewrite (sum_skipF (permutF _ _) ord0) (sum_skipF u (p ord0)); f_equal.
rewrite skipF_permutF IHn; try apply skip_f_ord_inj; easy.
Qed.
Lemma sum_revF : ∀ {n} (u : 'G^n), sum (revF u) = sum u.
Proof. intros; apply sum_permutF, rev_ord_inj. Qed.
Lemma sum_moveF : ∀ {n} (u : 'G^n.+1) i0 i1, sum (moveF u i0 i1) = sum u.
Proof. intros; apply sum_permutF, move_ord_inj. Qed.
Lemma sum_transpF : ∀ {n} (u : 'G^n) i0 i1, sum (transpF u i0 i1) = sum u.
Proof. intros; apply sum_permutF, transp_ord_inj. Qed.
Lemma sum_splitPF : ∀ {n} P (u : 'G^n), sum (splitPF P u) = sum u.
Proof.
intros n P u; induction n as [| n IHn].
rewrite sum_nil sum_nil'// !lenPF_nil; easy.
unfold splitPF; rewrite sum_concatF sum_ind_l;
destruct (classic (P ord0)) as [H0 | H0].
rewrite filterPF_ind_l_in (filterPF_ind_l_out (PNNP H0)).
rewrite !sum_castF sum_concatF sum_singleF -plus_assoc; f_equal.
unfold splitPF in IHn; rewrite -(IHn (liftF_S P)) sum_concatF; easy.
rewrite filterPF_ind_l_out filterPF_ind_l_in.
rewrite !sum_castF sum_concatF sum_singleF plus_assoc
(plus_comm _ (u ord0)) -plus_assoc; f_equal.
unfold splitPF in IHn; rewrite -(IHn (liftF_S P)) sum_concatF; easy.
Qed.
Lemma sum_itemF : ∀ {n} (x : G) i0, sum (itemF n x i0) = x.
Proof.
intros [| n] x i0; [now destruct i0 |].
unfold itemF; generalize (sum_replaceF (0 : 'G^n.+1) x i0).
rewrite sum_zero plus_zero_l plus_zero_r; easy.
Qed.
Lemma sum_split0F : ∀ {n} (u : 'G^n), sum (split0F u) = sum u.
Proof. intros; apply sum_splitPF. Qed.
Lemma sum_filter_n0F : ∀ {n} (u : 'G^n), sum u = sum (filter_n0F u).
Proof.
intros; rewrite -sum_split0F sum_concatF
-{2}(plus_zero_l (sum (filter_n0F u))); f_equal.
apply sum_zero_compat, filter0F_correct.
Qed.
Lemma sum_unfun0F :
∀ {n1 n2} (f : 'I_{n1,n2}) (u1 : 'G^n1),
injective f → sum (unfun0F f u1) = sum u1.
Proof.
intros n1 n2 f u1 Hf.
destruct (@unfun0F_eq G _ _ f Hf) as [p [Hp1 Hp2]].
rewrite Hp2 sum_permutF// sum_castF sum_concatF sum_zero plus_zero_r; easy.
Qed.
End Sum_Facts1.
Section Sum_Facts2.
Context {G : AbelianMonoid}.
Lemma sum_skipTc :
∀ {m n} (u : 'G^{m,n.+1}) j0, sum (skipTc u j0) = skipF (sum u) j0.
Proof.
intros; unfold skipTc, skipF.
apply extF; intro; rewrite 2!fct_sum_eq; easy.
Qed.
Lemma sum_row : ∀ {m n} (u : 'G^{m,n}) i, sum (row u i) = sum (col u) i.
Proof.
intros m n u i; induction n as [| n Hn]; try now rewrite 2!sum_nil.
rewrite 2!sum_ind_l fct_plus_eq fct_sum_eq; f_equal.
Qed.
Lemma sum_col : ∀ {m n} (u : 'G^{m,n}) i, sum (col u i) = sum (row u) i.
Proof.
intros m n u i; induction m as [|m Hm]; try now rewrite 2!sum_nil.
rewrite 2!sum_ind_l fct_plus_eq fct_sum_eq; f_equal.
Qed.
Lemma sumT_sym :
∀ {m n} (u : 'G^{m,n}), sum (sum u) = sum (sum (flipT u)).
Proof.
apply (nat_ind2 (fun m n ⇒
∀ u : 'G^{m,n}, sum (sum u) = sum (sum (flipT u)))).
intros; rewrite 2!sum_nil; easy.
move=>> H u; rewrite 2!(sum_skipF _ ord0) sum_plus sum_row H -sum_skipTc; easy.
move=>> H u; rewrite 2!(sum_skipF _ ord0) sum_plus sum_col -H sum_skipTc; easy.
Qed.
Functions to Abelian monoid.
Context {U : Type}.
Lemma sum_fun_compat : ∀ {n} (f : '(U → G)^n) x, sum f x = sum (f^~ x).
Proof.
intros n; induction n as [| n Hn]; intros f x.
rewrite 2!sum_nil; easy.
rewrite 2!sum_ind_l fct_plus_eq Hn; easy.
Qed.
End Sum_Facts2.
Section Sum_Facts3.
Context {G : AbelianMonoid}.
Context {T1 T2 : Type}.
Lemma sum_compF_l:
∀ {n} (u : '(T2 → G)^n) (f : T1 → T2), sum (compF_l u f) = sum u \o f.
Proof.
intros; apply fun_ext; intro;
rewrite comp_correct compF_l_correct fct_sum_eq -fct_sum_eq; easy.
Qed.
End Sum_Facts3.
Local Open Scope R_scope.
Section Sum_R_Facts.
Lemma sum_monot_R :
∀ {n} (u v : 'R^n), (∀ i, u i ≤ v i) → sum u ≤ sum v.
Proof.
intros n u v H; induction n as [| n Hn].
rewrite !sum_nil; apply Rle_refl.
rewrite !sum_ind_l; apply Rplus_le_compat; [apply H | apply Hn].
intros i; unfold liftF_S; easy.
Qed.
Lemma sum_nonneg_R :
∀ {n} (u : 'R^n), (∀ i, 0 ≤ u i) → 0 ≤ sum u.
Proof.
intros; replace 0 with (@zero R_AbelianMonoid); try easy.
rewrite -(@sum_zero _ n); apply sum_monot_R; easy.
Qed.
Lemma sum_nonneg_ub_R :
∀ {n} (u : 'R^n) i, (∀ i, 0 ≤ u i) → u i ≤ sum u.
Proof.
intros [| n] u i Hx; [now destruct i |].
rewrite (sum_skipF _ i) -{1}(plus_zero_r (u i)); apply Rplus_le_compat;
[apply Rle_refl | apply sum_nonneg_R].
intros; unfold skipF; easy.
Qed.
Lemma sum_def_R :
∀ {n} (u : 'R^n), (∀ i, 0 ≤ u i) → sum u = 0 → u = 0%M.
Proof.
intros n; induction n. intros; apply hat0F_unit.
intros u Hu; rewrite sum_ind_l.
assert (Hun : ∀ i, (0 ≤ liftF_S u i)%R) by (intros; apply Hu).
move⇒ /(Rplus_eq_R0 _ _ (Hu ord0) (sum_nonneg_R _ Hun)) [H0 Hn].
apply extF_zero_ind_l; [| apply IHn]; easy.
Qed.
End Sum_R_Facts.
Local Close Scope R_scope.
Local Open Scope nat_scope.
Section Sum_nat_Facts.
Lemma sum_constF_nat : ∀ {n} (x : nat), (sum (constF n x) = n × x)%coq_nat.
Proof.
intros n; induction n; intros x.
rewrite sum_nil; easy.
rewrite sum_ind_l; simpl.
apply trans_eq with (x+n×x).
2: auto with arith.
f_equal; rewrite <- IHn; try easy.
Qed.
Lemma sum_le_nat :
∀ {n} (u v : 'nat^n),
(∀ i, (u i ≤ v i)%coq_nat) → (sum u ≤ sum v)%coq_nat.
Proof.
intros n; induction n.
intros u v _; rewrite 2!sum_nil; easy.
intros u v H; rewrite 2!sum_ind_l.
apply Nat.add_le_mono; try easy.
apply IHn; intros i; apply H.
Qed.
Lemma sum_le_nat_gen :
∀ {n m} (u : 'nat^n) (v : 'nat^m) (H : n ≤ m),
(∀ i, (u i ≤ v (widen_ord H i))%coq_nat) → (sum u ≤ sum v)%coq_nat.
Proof.
intros n m u v H H1.
rewrite -(@sum_concatF_zero_r _ _ (m-n) u).
assert (V: (n + (m - n)) = m).
unfold plus; simpl; rewrite -minusE.
assert (n ≤ m)%coq_nat.
apply /leP; auto.
auto with zarith arith.
rewrite -(sum_castF V).
apply sum_le_nat.
intros i; unfold castF.
case (Nat.le_gt_cases n i); intros H2.
rewrite concatF_correct_r; simpl; auto with zarith.
intros H3; unfold zero; simpl; unfold fct_zero; simpl; auto with arith.
rewrite concatF_correct_l; auto with arith.
apply Nat.le_trans with (1:=H1 _).
apply Nat.eq_le_incl; f_equal; apply ord_inj; now simpl.
Qed.
Lemma sum_ub_nat : ∀ {n} (u : 'nat^n) i, (u i ≤ sum u)%coq_nat.
Proof.
intros [| n] u i; [now destruct i |].
replace (u i) with (sum (replaceF (constF n.+1 0%nat) (u i) i)).
apply sum_le_nat.
intros j.
case (ord_eq_dec j i); intros Hij.
rewrite replaceF_correct_l Hij; easy.
rewrite replaceF_correct_r; try easy.
rewrite constF_correct; auto with arith.
rewrite <- (Nat.add_0_l (sum _)).
replace 0%nat with (constF n.+1 0%nat i) at 1 by easy.
generalize (sum_replaceF (constF n.+1 0) (u i) i).
unfold plus; simpl; intros T; rewrite T.
rewrite sum_constF_nat.
rewrite Nat.mul_0_r; auto with zarith.
Qed.
Lemma sum_def_nat : ∀ {n} (u : 'nat^n), sum u = 0 → u = 0%M.
Proof.
intros n; induction n. intros; apply hat0F_unit.
intros u; rewrite sum_ind_l; move⇒ /nat_plus_def [H0 /IHn Hn].
apply extF_zero_ind_l; easy.
Qed.
End Sum_nat_Facts.
Local Open Scope Monoid_scope.
Section Sum_part_Facts.
Context {G : AbelianMonoid}.
Definition sum_part {n} (b : 'G^n) (i : 'I_n.+1) :=
sum (firstF (castF_nip b i)).
Lemma sum_part_nil :
∀ {n} (b : 'G^n) i, nat_of_ord i = 0 → sum_part b i = 0.
Proof.
intros n b i Hi; unfold sum_part.
replace i with (ord0: 'I_n.+1).
simpl; apply sum_nil.
apply ord_inj; easy.
Qed.
Lemma sum_part_ord_max : ∀ {n} (b : 'G^n.+1), sum_part b ord_max = sum b.
Proof.
intros n b; unfold sum_part.
unfold castF_nip, castF, firstF; simpl.
apply sum_ext; intros i; f_equal.
apply ord_inj; simpl; easy.
Qed.
Lemma sum_part_ind_r :
∀ {n} (b : 'G^n) i,
sum_part b (lift_S i) = sum_part b (widen_S i) + b i.
Proof.
intros n b i; unfold sum_part.
rewrite sum_ind_r; f_equal.
apply sum_ext; intros j.
unfold widenF_S, firstF, castF_nip, castF; simpl.
f_equal; apply ord_inj; now simpl.
unfold firstF, castF_nip, castF; simpl.
f_equal; apply ord_inj; now simpl.
Qed.
Lemma sum_part_ind_l :
∀ {n} (b : 'G^n.+1) i (H : i ≠ ord0),
sum_part b i = b ord0 + sum_part (liftF_S b) (lower_S H).
Proof.
intros n b i H; unfold sum_part.
pose (j:= lower_S H); fold j.
assert (H1 : lift_S j = i).
apply lift_lower_S.
rewrite <- H1.
rewrite sum_ind_l; f_equal.
unfold firstF, castF_nip, castF; simpl.
f_equal; apply ord_inj; now simpl.
apply sum_ext; intros k.
unfold liftF_S, lift_S, widenF_S, firstF, castF_nip, castF; simpl.
f_equal; apply ord_inj; now simpl.
Qed.
Lemma sum_part_ind_l_alt :
∀ {n} (b : 'G^n.+1) i (H : i ≠ ord0),
sum_part b (widen_S i) =
b ord0 + sum_part (liftF_S b) (widen_S (lower_S H)).
Proof.
intros n b i H.
assert (H' : widen_S i ≠ ord0)
by now apply ord_neq; apply ord_neq_compat in H.
rewrite sum_part_ind_l; repeat f_equal; apply ord_inj; easy.
Qed.
End Sum_part_Facts.
Section Sum_part_nat_Facts.
Lemma sum_ub_alt_nat :
∀ {d} (b : 'nat^d) k i, (sum b ≤ k)%coq_nat → (b i ≤ k)%coq_nat.
Proof.
intros d b k i H.
apply Nat.le_trans with (2:=H).
apply sum_ub_nat.
Qed.
Lemma sum_part_nat_monot_aux :
∀ {n} (b : 'nat^n) (i : 'I_n.+1) j (H : (i + j)%coq_nat < n.+1),
(sum_part b i ≤ sum_part b (Ordinal H))%coq_nat.
Proof.
intros n b i j; induction j; intros H.
apply Nat.eq_le_incl; f_equal.
apply ord_inj; simpl; auto with arith zarith.
assert (H': (i + j)%coq_nat < n.+1).
apply leq_ltn_trans with (2:=H).
apply /leP; auto with arith.
apply Nat.le_trans with (1:=IHj H').
assert (H'': (i + j)%coq_nat < n).
apply /ltP.
assert ((i+j.+1)%coq_nat < n.+1)%coq_nat by now apply /ltP.
auto with arith zarith.
apply Nat.le_trans with (sum_part b (widen_S (Ordinal H''))).
apply Nat.eq_le_incl; f_equal.
apply ord_inj; simpl; auto with arith zarith.
apply Nat.le_trans with (sum_part b (widen_S (Ordinal H'')) + b (Ordinal H'')).
auto with arith.
rewrite -sum_part_ind_r.
apply Nat.eq_le_incl; f_equal.
apply ord_inj; simpl; auto with arith zarith.
rewrite bump_r; auto with arith zarith.
Qed.
Lemma sum_part_nat_monot :
∀ {n} (b : 'nat^n) (i j : 'I_n.+1),
(i ≤ j)%coq_nat → (sum_part b i ≤ sum_part b j)%coq_nat.
Proof.
intros n b i j Hij.
pose (k:=(j-i)%coq_nat).
assert (H: (i+k)%coq_nat < n.+1).
unfold k; apply /ltP.
apply Nat.le_lt_trans with j.
auto with zarith.
destruct j; intros; simpl; apply /ltP; easy.
replace j with (Ordinal H).
apply sum_part_nat_monot_aux.
apply ord_inj; simpl.
unfold k; auto with zarith.
Qed.
End Sum_part_nat_Facts.