proposition: Lemma Diffble_I_scal : forall c : IR, Diffble_I Hab' (c{**}F).
proof: Proof. intro. unfold Fscalmult in |- *. apply Diffble_I_mult. apply Diffble_I_const. assumption. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps