fact: Definition domainWeaveOddInc {R : ConstructiveReals} (X : Set) (fn gn : nat -> @PartialFunction R X) (n : nat) (x : X) (xD : Domain (weaveSequences _ fn gn (1+n*2)) x) : Domain (gn n) x.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase