proposition: Lemma sum_by_packets : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) (Pn : nat -> nat) (n : nat), (forall k, le k n -> lt (Pn k) (Pn (S k))) -> Pn O = O -> CRsum (fun i => CRsum (fun k => xn (k + Pn i))%nat (pred (Pn (S i) - Pn i))) n == CRsum xn (pred (Pn (S n))).
proof: Proof. induction n. - intros. simpl. rewrite H0. replace (pred (Pn 1 - 0))%nat with (pred (Pn 1%nat)). apply CRsum_eq. intros. rewrite Nat.add_comm. reflexivity. rewrite Nat.sub_0_r. reflexivity. - intros. assert (forall k : nat, k <= n -> Pn k < Pn (S k))%nat. { intros. apply H. apply (Nat.le_trans _ n _ H1). apply le_S, Nat.le_refl. } specialize (IHn H1 H0). clear H1. simpl. rewrite IHn. destruct (Pn (S (S n)) - Pn (S n))%nat eqn:des. exfalso. apply Nat.sub_0_le in des. apply (proj1 (Nat.le_ngt _ _) des). apply H, Nat.le_refl. simpl. pose proof (H n). destruct (Pn (S n)). exfalso. apply (proj1 (Nat.le_ngt 0 (Pn n)) (Nat.le_0_l _)). apply H1, le_S, Nat.le_refl. clear H1. simpl. rewrite (CRsum_eq (fun k : nat => xn (k + S n1)%nat) (fun k : nat => xn (S n1 + k)%nat)). 2: intros; rewrite Nat.add_comm; reflexivity. rewrite <- (sum_assoc xn n1). replace (S n1 + n0)%nat with (Init.Nat.pred (Pn (S (S n)))). reflexivity. pose proof (H (S n) (Nat.le_refl _)). destruct (Pn (S (S n))). exfalso. inversion H1. simpl. simpl in des. replace (S (n1 + n0)) with (n1 + S n0)%nat. 2: apply Nat.add_succ_r. rewrite <- des. rewrite Nat.add_comm. rewrite Nat.sub_add. reflexivity. destruct (le_lt_dec n2 n1). apply Nat.sub_0_le in l. rewrite l in des. discriminate. apply (Nat.le_trans _ (S n1)). apply le_S, Nat.le_refl. exact l. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal