proposition: Lemma compact_interval_inc : forall I (cI : compact_ I) H, included (compact (Lend cI) (Rend cI) H) I.
proof: Proof. intros [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI. generalize c c0 cI H; clear H cI c0 c. simpl in |- *; intros a b Hab. intros H x H0. inversion_clear H0; split; auto. Qed.
imports: CoRN.ftc.NthDerivative