proposition: Lemma FSumx_lt : forall n (f : forall i, i < n -> PartIR), ext_fun_seq f -> forall i Hi x Hx Hx', FSumx_to_FSum n f i x Hx [=] f i Hi x Hx'.
proof: Proof. do 6 intro. unfold FSumx_to_FSum in |- *. elim (le_lt_dec n i); intro; simpl in |- *. exfalso; apply (Nat.le_ngt n i); auto. intros; apply H; auto. algebra. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality