proposition: Lemma str_Sumx_Sum_Sum : forall n (g : (forall i Hi, nat -> F)), (forall i j Hi, f i <= j -> j < f (S i) -> g i Hi j [=] h j) -> forall m, m = f n -> Sumx (fun i (H : i < n) => Sum (f i) (pred (f (S i))) (g i H)) [=] Sumx (fun i (H : i < m) => h i).
proof: Proof. intros. rewrite H0. eapply eq_transitive_unfolded. 2: apply Sumx_Sum_Sum. apply Sumx_wd. intros. apply Sum_wd'. cut (0 < f (S i)); [ intro | rewrite <- f0; auto with arith ]. cut (f (S i) = S (pred (f (S i)))); [ intro | symmetry; apply Nat.lt_succ_pred with 0; auto ]. rewrite <- H3. apply Nat.lt_le_incl; auto with arith. intros; apply H. assumption. rewrite <- (Nat.lt_succ_pred 0 (f (S i))); auto with arith. rewrite <- f0; auto with arith. Qed.
imports: CoRN.algebra.COrdCauchy Coq(Lia)