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