proposition: Lemma interval_compact_inc : forall I (cI : compact_ I) H, included I (compact (Lend cI) (Rend cI) H).
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 Hab'. intros x H. simpl in H. inversion_clear H; split; auto. Qed.
imports: CoRN.ftc.NthDerivative