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