proposition: Lemma included_comp' : included (Compact Hab) (Dom (G'[o]F)).
proof: Proof. intros x H. simpl in |- *. exists (derivative_imp_inc _ _ _ _ _ derF x H). apply (derivative_imp_inc' _ _ _ _ _ derG). apply maps_lemma' with G a b Hab; assumption. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries