proposition: Lemma FSum_FSumx_to_FSum : forall n (f : forall i, i < S n -> PartIR), ext_fun_seq f -> ext_fun_seq' f -> forall x Hx Hx', FSum 0 n (FSumx_to_FSum _ f) x Hx [=] FSumx _ f x Hx'.
proof: Proof. simple induction n. intros; simpl in |- *. eapply eq_transitive_unfolded. apply Sum_one. simpl in |- *. cut (0 < 1); [ intro | apply Nat.lt_succ_diag_r ]. astepr (Part (f 0 (Nat.lt_succ_diag_r 0)) x (ProjIR2 Hx')). apply FSumx_lt; assumption. clear n; intros n H f H0 H1 x Hx Hx'. simpl in |- *. eapply eq_transitive_unfolded. apply Sum_last. apply bin_op_wd_unfolded. set (g := fun i (l : i < S n) => f i (Nat.lt_lt_succ_r _ _ l)) in *. cut (ext_fun_seq g); intros. cut (ext_fun_seq' g). intro H3. astepr (FSumx n (fun i (l : i < n) => g i (Nat.lt_lt_succ_r _ _ l)) x (ProjIR1 (ProjIR1 Hx')) [+]g n (Nat.lt_succ_diag_r n) x (ProjIR2 (ProjIR1 Hx'))). cut (Dom (FSumx _ g) x). intro H4; cut (forall m : nat, Dom (FSumx_to_FSum (S n) g m) x). intro Hx''. simpl in H. apply eq_transitive_unfolded with (Sum 0 n (fun m : nat => FSumx_to_FSum (S n) g m x (Hx'' m))). 2: apply H with (f := g); try assumption. apply Sum_wd'. auto with arith. intros. cut (i < S (S n)); [ intro | auto with arith ]. apply eq_transitive_unfolded with (f i H7 x (FSumx_pred _ _ H1 x Hx' i H7)). apply FSumx_lt; assumption. cut (i < S n); [ intro | auto with arith ]. apply eq_transitive_unfolded with (g i H8 x (FSumx_pred _ _ H3 x H4 i H8)). 2: apply eq_symmetric_unfolded; apply FSumx_lt; assumption. unfold g in |- *; apply H0; auto. algebra. intro. simpl in Hx. generalize (Hx m); clear H4 H3 H2 Hx. unfold FSumx_to_FSum in |- *. elim (le_lt_dec (S n) m); elim (le_lt_dec (S (S n)) m); do 2 intro; simpl in |- *; intro. auto. auto. unfold g in |- *; apply FSumx_pred with (n := S (S n)); assumption. unfold g in |- *; apply FSumx_pred with (n := S (S n)); assumption. simpl in Hx'. unfold g in |- *; inversion_clear Hx'; intros; assumption. unfold g in |- *; red in |- *; intros. red in H1; apply H1 with i (Nat.lt_lt_succ_r _ _ Hi) x0; auto. unfold g in |- *; red in |- *; intros. red in H0; apply H0; auto. apply FSumx_lt; auto. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality