proposition: Lemma compact_in_interval_wd1 : forall I pI x Hx y Hy (H : compact_ (compact_in_interval I pI x Hx)) (H' : compact_ (compact_in_interval I pI y Hy)), x [=] y -> Lend H [=] Lend H'.
proof: Proof. intro I; elim I; simpl in |- *; intros; algebra. Qed.
imports: CoRN.ftc.NthDerivative