proposition: Lemma Diffble_I_Sumx : forall n (f : forall i, i < n -> PartIR), (forall i Hi, Diffble_I Hab' (f i Hi)) -> Diffble_I Hab' (FSumx n f).
proof: Proof. intro; induction n as [| n Hrecn]; intros. simpl in |- *; apply Diffble_I_const. simpl in |- *. apply Diffble_I_plus; auto. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps