proposition: Lemma Derivative_scal : forall c : IR, Derivative I pI (c{**}F) (c{**}F').
proof: Proof. intro. elim derF; intros incF H. elim H; intros incF' derivF. split. Included. split; Deriv. Qed.
imports: CoRN.ftc.MoreIntervals