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