proposition: Lemma N_Deriv_wd : forall x y Hx Hy, x [=] y -> N_Deriv_fun x Hx [=] N_Deriv_fun y Hy.
proof: Proof. intros. apply not_ap_imp_eq. intro H0. cut (x [#] y). apply eq_imp_not_ap; auto. exact (N_Deriv_strext _ _ _ _ H0). Qed.
imports: CoRN.ftc.MoreIntervals