proposition: Lemma Diffble_I_comp : Diffble_I Hab' (G[o]F).
proof: Proof. elim diffF; intros f' derF. elim diffG; intros g' derG. apply Diffble_I_comp_aux with (PartInt f') (PartInt g') c d Hcd'; auto. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries