fact: Definition Derivative_n (pI : proper I) F G := included I (Dom F) and included I (Dom G) and (forall a b Hab, included (Compact (less_leEq _ a b Hab)) I -> Derivative_I_n Hab n F G).
imports: CoRN.ftc.NthDerivative