proposition: Lemma included_imp_contin : forall c d Hcd, included (compact c d Hcd) (Compact Hab) -> Continuous_I Hab F -> Continuous_I Hcd F.
proof: Proof. intros c d Hcd H H0. elim H0; clear H0; intros incF' contF. split. apply included_trans with (Compact Hab); [ apply H | apply incF' ]. intros e He; elim (contF e He); intros e' H0 H1. exists e'. assumption. intros; apply H1. apply H; assumption. apply H; assumption. assumption. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac