proposition: Lemma Diffble_I_plus : Diffble_I Hab' (F{+}G).
proof: Proof. elim diffF; intros F' derF. elim diffG; intros G' derG. exists (IPlus F' G'). eapply Derivative_I_wdr. apply part_int_plus with (F := PartInt F') (G := PartInt G'). apply Feq_reflexive; Included. apply Feq_reflexive; Included. Deriv. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps