proposition: Lemma ConstFilter_length : forall (b:bool) (n:nat), length (ConstFilter b n) = n.
proof: Proof. induction n. reflexivity. simpl. apply f_equal, IHn. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile