fact: Definition DiscrDeriv {R : ConstructiveReals} (X : Set) (fn : nat -> @PartialFunction R X) (n : nat) := match n with | O => fn O | S p => Xminus (fn n) (fn p) end.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions