fact: Fixpoint ConstFilter (b : bool) (n : nat) : list bool := match n with | O => nil | S p => b :: ConstFilter b p end.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile