fact: Hypothesis P_Derivable2 : forall m n k f le, P (Derivable2 m n k f le).
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct