proposition: Lemma included_imp_deriv : forall a b Hab c d Hcd F F', included (compact c d (less_leEq _ _ _ Hcd)) (compact a b (less_leEq _ _ _ Hab)) -> Derivative_I Hab F F' -> Derivative_I Hcd F F'.
proof: Proof. intros a b Hab c d Hcd F F' H H0. elim H0; clear H0; intros incF H0. elim H0; clear H0; intros incF' H0. apply Derivative_I_char. apply included_trans with (Compact (less_leEq _ _ _ Hab)); auto. apply included_trans with (Compact (less_leEq _ _ _ Hab)); auto. intros e He; elim (H0 e He); intros e' He'. exists e'; auto. Qed.
imports: CoRN.ftc.Continuity