proposition: Lemma FreeSubsetsFull : forall l : list bool, { k : nat | lt k (length (FreeSubsets (length l))) /\ nth k (FreeSubsets (length l)) nil = l }.
proof: Proof. induction l as [|a l]. - exists O. split. apply Nat.le_refl. reflexivity. - simpl. destruct IHl as [k [H H0]]. destruct a. + exists k. split. rewrite app_length, map_length, map_length. apply (Nat.lt_le_trans _ (0+length (FreeSubsets (length l)))). exact H. rewrite <- Nat.add_le_mono_r. apply Nat.le_0_l. rewrite app_nth1. rewrite (nth_indep _ nil (true::nil)), map_nth, H0. reflexivity. rewrite map_length. exact H. rewrite map_length. exact H. + exists (k + length (FreeSubsets (length l)))%nat. split. rewrite app_length, map_length, map_length. rewrite <- Nat.add_lt_mono_r. exact H. rewrite app_nth2. rewrite map_length, Nat.add_sub. rewrite (nth_indep _ nil (false::nil)), map_nth, H0. reflexivity. rewrite map_length. exact H. rewrite map_length. apply (Nat.le_trans _ (0+length (FreeSubsets (length l)))). apply Nat.le_refl. rewrite <- Nat.add_le_mono_r. apply Nat.le_0_l. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile