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.

Brief description

Support for the iteration of the commutative monoid law.

Description

Let G be an AbelianMonoid. Let u be an n-family of G.
  • 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.
Let G1 G2 : AbelianMonoid. Let f : G1 G2.

Used logic axioms

  • classic, the weak form of excluded middle.

Usage

This module may be used through the import of Algebra.Monoid.Monoid, Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

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; rewriteinsertF_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; rewritereplace2F_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.