proposition: Lemma Diffble_I_mult : Diffble_I Hab' (F{*}G).
proof: Proof. elim diffF; intros F' derF. elim diffG; intros G' derG. exists (IPlus (IMult (IntPartIR (diffble_imp_inc _ _ _ _ diffF)) G') (IMult F' (IntPartIR (diffble_imp_inc _ _ _ _ diffG)))). eapply Derivative_I_wdr. apply part_int_plus with (F := PartInt (IMult (IntPartIR (diffble_imp_inc _ _ _ _ diffF)) G')) (G := PartInt (IMult F' (IntPartIR (diffble_imp_inc _ _ _ _ diffG)))). apply Feq_reflexive; Included. apply Feq_reflexive; Included. eapply Derivative_I_wdr. apply Feq_plus with (F := F{*}PartInt G') (G := PartInt F'{*}G). apply part_int_mult. FEQ. apply Feq_reflexive; Included. apply part_int_mult. apply Feq_reflexive; Included. FEQ. Deriv. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps