proposition: Lemma FSumx_pred : forall n (f : forall i, i < n -> PartIR), ext_fun_seq' f -> forall x, Dom (FSumx n f) x -> forall i Hi, Dom (f i Hi) x.
proof: Proof. intros n f H x H0 i Hi; red in H; induction n as [| n Hrecn]. exfalso; inversion Hi. elim (le_lt_eq_dec _ _ Hi); intro. cut (i < n); [ intro | auto with arith ]. set (g := fun i Hi => f i (Nat.lt_lt_succ_r _ _ Hi)) in *. apply H with i (Nat.lt_lt_succ_r _ _ H1) x. auto. algebra. change (Dom (g i H1) x) in |- *. apply Hrecn. unfold g in |- *; intros. apply H with i0 (Nat.lt_lt_succ_r i0 n Hi0) x0; auto. inversion_clear H0; assumption. elim H0; intros H1 H2; clear H0 H1. apply H with n (Nat.lt_succ_diag_r n) x; auto. symmetry in |- *; auto. algebra. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality