proposition: Lemma iprop_compact_in_interval' : forall I pI x Hx (H : compact_ (compact_in_interval I pI x Hx)) H', compact (Lend H) (Rend H) H' x.
proof: Proof. do 4 intro. cut (compact_in_interval I pI x Hx x). 2: apply iprop_compact_in_interval. elim (compact_in_interval I pI x Hx); intros; try inversion H. simpl in |- *; auto. Qed.
imports: CoRN.ftc.NthDerivative