proposition: Lemma Diffble_I_Sum0 : forall (f : nat -> PartIR), (forall n, Diffble_I Hab' (f n)) -> forall n, Diffble_I Hab' (FSum0 n f).
proof: Proof. intros f diffF. induction n as [| n Hrecn]. apply Diffble_I_wd with (Fconst (S:=IR) [0]). apply Diffble_I_const. FEQ. red in |- *; simpl in |- *; intros. apply (diffble_imp_inc _ _ _ _ (diffF n)); assumption. apply Diffble_I_wd with (FSum0 n f{+}f n). apply Diffble_I_plus. auto. auto. FEQ. simpl in |- *; red in |- *; intros. apply (diffble_imp_inc _ _ _ _ (diffF n0)); assumption. simpl in |- *. apply bin_op_wd_unfolded; try apply Sum0_wd; intros; rational. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps