proposition: Lemma pick_variety_auxCP_forallT {m : nat} : forall s (cp : cartesianPower positive (S (S m))), pick_variety_auxCP s cp = true <-> (forall p, InCP p cp -> S.mem p s = true).
proof: Proof. induction m; intros s cp; [unfold InCP|]; simpl; split. { intro Hmem; apply andb_true_iff in Hmem; destruct Hmem as [Hmem1 Hmem2]. intros p H; do 2 (try (elim H; clear H; intro; subst)); auto. } { intro H; apply andb_true_iff; split; [apply (H (fst cp))|apply (H (snd cp))]; auto. } { intro Hmem; apply andb_true_iff in Hmem; destruct Hmem as [Hmem1 Hmem2]. intros p H; apply InCPOK in H; elim H; clear H; intro HIn; subst; simpl; auto. destruct (IHm s (tailCP cp)) as [H _]; apply H; auto. } { destruct (IHm s (tailCP cp)) as [_ H]; clear IHm; rename H into IHm. intro H; apply andb_true_iff; split; [apply (H (fst cp))|apply IHm; intros p HIn; apply H]; apply InCPOK; auto. } Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets