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