proposition: Lemma pick_variety_aux_memCPAux2 : forall s1 s2 m (cp : cartesianPower positive (S (S m))), pick_variety_auxCP (S.inter s1 s2) cp = true -> memCPAux m cp s2 = true.
proof: Proof. intros s1 s2 m cp. induction m; simpl; do 2 (rewrite andb_true_iff); intro Hhtspa. do 2 (rewrite SWP.FM.inter_b in Hhtspa). do 2 (rewrite andb_true_iff in Hhtspa). tauto. destruct Hhtspa as [Hmem Hhtspa]. rewrite SWP.FM.inter_b in Hmem. rewrite andb_true_iff in Hmem. split; try (spliter; assumption). apply IHm; assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets