proposition: Lemma Derivative_n_wdl : forall n F G H, Feq I F G -> Derivative_n n I pI F H -> Derivative_n n I pI G H.
proof: Proof. intros n F G H H0 H1. elim H0; intros incG H2. elim H2; intros incH Heq. elim H1; intros incF H0'. elim H0'; intros incG' derivF. clear H2 H0'. split; auto. split; auto. intros; apply Derivative_I_n_wdl with F. apply included_Feq with I; auto. auto. Qed.
imports: CoRN.ftc.MoreIntervals