proposition: Lemma str_Sumx_Sum_Sum' : forall (m : nat) (f : forall i, i <= m -> nat), f 0 (Nat.le_0_l _) = 0 -> (forall (i j : nat) Hi Hj, i = j -> f i Hi = f j Hj) -> (forall (i j : nat) Hi Hj, i < j -> f i Hi < f j Hj) -> forall (h : nat -> F) (n : nat) (g : forall i : nat, i < m -> nat -> F), (forall (i j : nat) Hi Hi' Hi'', f i Hi' <= j -> j < f (S i) Hi'' -> g i Hi j [=] h j) -> (forall H, n = f m H) -> Sumx (fun (i : nat) (H : i < m) => Sum (f i (Nat.lt_le_incl _ _ H)) (pred (f (S i) H)) (g i H)) [=] Sumx (fun (i : nat) (_ : i < n) => h i).
proof: Proof. intros. cut (forall (i : nat) (H : i <= m), f i H = f' m f i). intros. apply eq_transitive_unfolded with (Sumx (fun (i : nat) (H3 : i < m) => Sum (f' m f i) (pred (f' m f (S i))) (g i H3))). apply Sumx_wd; intros. rewrite <- (H4 i (Nat.lt_le_incl _ _ H5)); rewrite <- (H4 (S i) H5); apply Sum_wd'. rewrite -> (Nat.lt_succ_pred (f i (Nat.lt_le_incl _ _ H5)) (f (S i) H5) (H1 _ _ _ _ (Nat.lt_succ_diag_r i))) . apply Nat.lt_le_incl; apply H1; apply Nat.lt_succ_diag_r. intros; algebra. apply str_Sumx_Sum_Sum. unfold f' in |- *; simpl in |- *. elim (le_lt_dec 0 m); intro; simpl in |- *. transitivity (f 0 (Nat.le_0_l m)). apply H0; auto. apply H. exfalso; inversion b. intros; apply nat_local_mon_imp_mon. clear H5 j i; intros. unfold f' in |- *. elim (le_lt_dec i m); elim (le_lt_dec (S i) m); intros; simpl in |- *. apply H1; apply Nat.lt_succ_diag_r. cut (i = m); [ intro | apply Nat.le_antisymm; auto with arith ]. generalize a; clear a; pattern i at 1 2 in |- *; rewrite H5; intro. set (x := f m a) in *. cut (x = f m (le_n m)). 2: unfold x in |- *; apply H0; auto. intro. rewrite <- H6. rewrite <- plus_n_Sm; auto with arith. exfalso; apply (Nat.le_ngt i m); auto with arith. set (x := f m (le_n m)) in *; clearbody x; auto with arith. assumption. intros. apply H2 with (Hi' := Nat.lt_le_incl _ _ Hi) (Hi'' := Hi). rewrite H4; assumption. rewrite H4; assumption. unfold f' in |- *. elim (le_lt_dec m m); intro; simpl in |- *. apply H3. elim (Nat.lt_irrefl _ b). clear H3 H2 g n h; intros. unfold f' in |- *. elim (le_lt_dec i m); intro; simpl in |- *. apply H0; auto. lia; auto. Qed.
imports: CoRN.algebra.COrdCauchy Coq(Lia)