proposition: Lemma included_compact_in_interval : forall I pI x Hx, included (compact_in_interval I pI x Hx) I.
proof: Proof. induction I; simpl in |- *; intros X x X0; try inversion_clear Hx; red in |- *; simpl in |- *; intros x0 X1; try inversion_clear X; try inversion_clear X0; try inversion_clear X1; auto. apply less_leEq_trans with x; auto. apply leEq_less_trans with x; auto. apply leEq_transitive with x; auto. apply leEq_transitive with x; auto. split. apply cip2' with x; auto. apply cip3' with x; auto. split. apply cip2' with x; auto. apply cip3 with x; auto. split. apply cip2 with x; auto. apply cip3' with x; auto. Qed.
imports: CoRN.ftc.NthDerivative