proposition: Lemma DiscrDerivDomainIncReverse : forall {R : ConstructiveReals} (X : Set) (fn : nat -> @PartialFunction R X) (x : X) (xn : forall n : nat, Domain (DiscrDeriv X fn n) x) (n : nat), Domain (fn n) x.
proof: Proof. intros. pose (xn n). unfold DiscrDeriv in d. destruct n. exact d. unfold Xminus, Xplus in d. exact (fst d). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions