proposition: Lemma Derivative_I_char : forall F F' (P:=Dom F) (P':=Dom F'), included I (Dom F) -> included I (Dom F') -> (forall e, [0] [<] e -> {d : IR | [0] [<] d | forall x y, I x -> I y -> forall Hx Hy Hx', AbsIR (x[-]y) [<=] d -> AbsIR (F y Hy[-]F x Hx[-]F' x Hx'[*] (y[-]x)) [<=] e[*]AbsIR (y[-]x)}) -> Derivative_I Hab' F F'.
proof: Proof. unfold Hab in |- *. intros. repeat (split; auto). Qed.
imports: CoRN.ftc.Continuity