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