fact: Definition PrependSeq {X : Type} (x : X) (un : nat -> X) (n : nat) := match n with | O => x | S p => un p end.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions