proposition: Lemma Derivative_mult : Derivative I pI (F{*}G) (F{*}G'{+}F'{*}G).
proof: Proof. elim derF; intros incF H. elim H; intros incF' derivF. elim derG; intros incG H'. elim H'; intros incG' derivG. split. Included. split. apply included_FPlus; Included. Deriv. Qed.
imports: CoRN.ftc.MoreIntervals