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