proposition: Lemma Derivative_I_wdr : Feq I F G -> Derivative_I Hab' H F -> Derivative_I Hab' H G.
proof: Proof. intros H0 H1. elim H0; intros incF H0'. elim H0'; intros incG Heq. elim H1; intros incH H2. elim H2; intros incF0 H3. apply Derivative_I_char; auto. intros e He. elim (H3 e He); clear H3; intros d H3 H4. exists d; auto. intros x y H5 H6 Hx Hy Hx' H7. astepl (AbsIR (H y Hy[-]H x Hx[-]F x (incF x H5) [*] (y[-]x))); auto. Qed.
imports: CoRN.ftc.Continuity