proposition: Lemma Sumx_Sum_Sum : forall n, Sumx (fun i (H : i < n) => Sum (f i) (pred (f (S i))) h) [=] Sumx (fun i (H : i < f n) => h i).
proof: Proof. simple induction n. rewrite f0; simpl in |- *; algebra. clear n; intros. elim (le_lt_dec n 0); intro. cut (n = 0); [ clear a; intro | auto with arith ]. rewrite H0 in H. rewrite H0. clear H0. simpl in |- *. astepl (Sum (f 0) (pred (f 1)) h). rewrite f0. apply eq_symmetric. eapply eq_transitive. apply Sumx_to_Sum. pattern 0 at 1 in |- *; rewrite <- f0; apply f_mon; apply Nat.lt_succ_diag_r. intros i j H0 H1 H'; rewrite H0; algebra. clear H; apply Sum_wd'; unfold part_tot_nat_fun in |- *; auto with arith. intros. elim (le_lt_dec (f 1) i); intro; simpl in |- *. cut (0 < f 1). intro; exfalso; lia. pattern 0 at 1 in |- *; rewrite <- f0; apply f_mon; apply Nat.lt_succ_diag_r. algebra. cut (0 < f n); [ intro | rewrite <- f0; apply f_mon; assumption ]. simpl in |- *. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply Sumx_to_Sum. apply eq_transitive_unfolded with (Sum 0 (pred (f n)) (part_tot_nat_fun _ _ (fun (i : nat) (H : i < f n) => h i)) [+] Sum (f n) (pred (f (S n))) h). apply bin_op_wd_unfolded. eapply eq_transitive_unfolded. apply H. apply Sumx_to_Sum; try assumption. red in |- *; intros; rewrite H1; algebra. algebra. cut (f n = S (pred (f n))); [ intro | symmetry; apply Nat.lt_succ_pred with 0; auto ]. setoid_rewrite H1 at 3. eapply eq_transitive_unfolded. 2: apply Sum_Sum with (m := pred (f n)). apply bin_op_wd_unfolded; apply Sum_wd'. rewrite <- H1; apply Nat.lt_le_incl; assumption. intros. elim (le_lt_dec (f n) i); intro; simpl in |- *. exfalso; lia. elim (le_lt_dec (f (S n)) i); intro; simpl in |- *. cut (f n < f (S n)); [ intro | apply f_mon; apply Nat.lt_succ_diag_r ]. exfalso; apply (Nat.le_ngt (f n) i); auto. apply Nat.le_trans with (f (S n)); auto with arith. intros; unfold part_tot_nat_fun in |- *; elim (le_lt_dec (f (S n)) i);elim (le_lt_dec (f n) i);simpl;intros; try reflexivity;try exfalso; try lia. rewrite <-H1; cut (0 < f (S n)); [ intro | rewrite <- f0; auto with arith ]; cut (f (S n) = S (pred (f (S n)))); [ intro | symmetry; apply Nat.lt_succ_pred with 0; auto ]; rewrite <- H3; apply Nat.lt_le_incl; auto with arith. intros; unfold part_tot_nat_fun in |- *;elim (le_lt_dec (f (S n)) i); [intro; simpl in |- *; exfalso; lia| reflexivity]. apply Nat.lt_trans with (f n); auto with arith. red in |- *; intros; rewrite -> H1; reflexivity. Qed.
imports: CoRN.algebra.COrdCauchy Coq(Lia)