proposition: Lemma Derivative_wdr : Feq I F G -> Derivative I pI H F -> Derivative I pI H G.
proof: Proof. intros H0 H1. elim H0; intros incF H0'. elim H0'; intros incG Heq. elim H1; intros incF' H1'. elim H1'; intros incH' derF. split. auto. split. auto. intros; apply Derivative_I_wdr with F; auto. apply included_Feq with I; auto. Qed.
imports: CoRN.ftc.MoreIntervals