proposition: Lemma FreeSubsetsNotNil : forall n : nat, FreeSubsets n <> nil.
proof: Proof. induction n. - discriminate. - simpl. intro abs. apply app_eq_nil in abs. destruct abs. apply map_eq_nil in H. exact (IHn H). Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile