proposition: Lemma Derivative_I_inv : Derivative_I Hab' {--}F {--}F'.
proof: Proof. clear derG. elim derF; intros incF H1. elim H1; intros incF' H2. clear H1. apply Derivative_I_char. Included. Included. intros e He. elim (H2 e He); intros d H0 H1. exists d. assumption. intros. simpl in |- *. apply leEq_wdl with (AbsIR [--](F y Hy[-]F x Hx[-]F' x Hx'[*](y[-]x))). eapply leEq_wdl. 2: apply AbsIR_inv. auto. apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.Derivative