proposition: Lemma Diffble_I_comp_aux : Diffble_I Hab' (G[o]F).
proof: Proof. elim derF; intros incF H1. elim H1; intros incF' H2. elim derG; intros incG H4. elim H4; intros incG' H5. clear H1 H4. exists (IntPartIR (included_FMult _ _ _ _ (included_comp _ _ _ _ _ _ _ _ incF incG' maps') incF')). eapply Derivative_I_wdr. 2: apply Derivative_I_comp. FEQ. exact (included_FMult _ _ _ _ (included_comp _ _ _ _ _ _ _ _ incF incG' maps') incF'). Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries