proposition: Lemma Derivative_n_O : forall F, included I (Dom F) -> Derivative_n 0 I pI F F.
proof: Proof. intros. split; Included. split; Included. intros. red in |- *; apply Feq_reflexive; Included. Qed.
imports: CoRN.ftc.MoreIntervals