proposition: Lemma memCPToSSOK {m : nat} : forall e (cp : cartesianPower positive (S m)), S.mem e (CPToSS cp) = true -> InCP e cp.
proof: Proof. induction m; intros e cp Hmem. unfold InCP. simpl in *. left. rewrite <- SWP.singleton_equal_add in Hmem. apply SWP.Dec.F.mem_2 in Hmem. apply SWP.Dec.F.singleton_1. assumption. apply InCPOK. rewrite CPToSSHdTl in Hmem. rewrite SWP.Dec.F.add_b in Hmem. rewrite <- SWP.Dec.F.singleton_b in Hmem. apply orb_true_iff in Hmem. elim Hmem; clear Hmem; intro Hmem. left. apply SWP.Dec.F.mem_2 in Hmem. apply SWP.Dec.F.singleton_1 in Hmem. intuition. right. apply IHm. assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets