proposition: Lemma FreeSubsetsDifferent : forall (n p q : nat), p <> q -> lt p (length (FreeSubsets n)) -> lt q (length (FreeSubsets n)) -> nth p (FreeSubsets n) nil <> nth q (FreeSubsets n) nil.
proof: Proof. induction n. - intros. exfalso. simpl in H0. simpl in H1. destruct p,q. exact (H eq_refl). apply le_S_n in H1. inversion H1. apply le_S_n in H0. inversion H0. apply le_S_n in H1. inversion H1. - intros. simpl. destruct (le_lt_dec (length (FreeSubsets n)) p), (le_lt_dec (length (FreeSubsets n)) q). + rewrite app_nth2. 2: rewrite map_length; exact l. rewrite app_nth2. 2: rewrite map_length; exact l0. rewrite map_length. assert (q - length (FreeSubsets n) < length (FreeSubsets n))%nat. { rewrite (Nat.add_lt_mono_r _ _ (length (FreeSubsets n))). rewrite Nat.sub_add. 2: exact l0. simpl in H1. rewrite app_length, map_length, map_length in H1. exact H1. } assert (p - length (FreeSubsets n) < length (FreeSubsets n))%nat. { rewrite (Nat.add_lt_mono_r _ _ (length (FreeSubsets n))). rewrite Nat.sub_add. 2: exact l. simpl in H0. rewrite app_length, map_length, map_length in H0. exact H0. } specialize (IHn (p - length (FreeSubsets n))%nat (q - length (FreeSubsets n))%nat). rewrite (nth_indep _ nil (false::nil)), (nth_indep _ nil (false::nil)). rewrite map_nth, map_nth. 2: rewrite map_length; exact H2. 2: rewrite map_length; exact H3. intro abs. inversion abs. apply IHn. 2: exact H3. 2: exact H2. 2: exact H5. intro abs2. assert ((p - length (FreeSubsets n) + length (FreeSubsets n))%nat = (q - length (FreeSubsets n) + length (FreeSubsets n))%nat). { rewrite abs2. reflexivity. } do 2 rewrite Nat.sub_add in H4. contradiction. exact l0. exact l. exact l. + clear IHn. rewrite app_nth2. 2: rewrite map_length; exact l. rewrite app_nth1. 2: rewrite map_length; exact l0. rewrite map_length. rewrite (nth_indep _ nil (false::nil)), (nth_indep _ nil (true::nil)). rewrite map_nth, map_nth. intro abs. inversion abs. rewrite map_length. exact l0. rewrite map_length. rewrite (Nat.add_lt_mono_r _ _ (length (FreeSubsets n))). rewrite Nat.sub_add. 2: exact l. simpl in H0. rewrite app_length, map_length, map_length in H0. exact H0. + clear IHn. rewrite app_nth1. 2: rewrite map_length; exact l. rewrite app_nth2. 2: rewrite map_length; exact l0. rewrite map_length. rewrite (nth_indep _ nil (true::nil)), (nth_indep _ nil (false::nil)). rewrite map_nth, map_nth. intro abs. inversion abs. rewrite map_length. rewrite (Nat.add_lt_mono_r _ _ (length (FreeSubsets n))). rewrite Nat.sub_add. 2: exact l0. simpl in H1. rewrite app_length, map_length, map_length in H1. exact H1. rewrite map_length. exact l. + rewrite app_nth1. 2: rewrite map_length; exact l. rewrite app_nth1. 2: rewrite map_length; exact l0. rewrite (nth_indep _ nil (true::nil)), (nth_indep _ nil (true::nil)). rewrite map_nth, map_nth. intro abs. inversion abs. apply (IHn p q H l l0). exact H3. rewrite map_length. exact l0. rewrite map_length. exact l. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile