proposition: Lemma FreeSubsetsLength : forall (n : nat) (l : list bool), In l (FreeSubsets n) -> length l = n.
proof: Proof. induction n. - intros. destruct H. subst l. reflexivity. exfalso; inversion H. - intros. simpl in H. apply in_app_or in H. destruct H. + apply in_map_iff in H. destruct H as [k [H H0]]. subst l. simpl. rewrite (IHn k). reflexivity. exact H0. + apply in_map_iff in H. destruct H as [k [H H0]]. subst l. simpl. rewrite (IHn k). reflexivity. exact H0. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile