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