proposition: Lemma CPToSSOK : forall (cp cp' : cartesianPower positive (S (S (S n)))) s, S.Equal (CPToSS cp) s -> memCP cp' s = true -> incl (CPToList cp') (CPToList cp).
proof: Proof. unfold incl. intros cp cp' s HEq Hmem e HIn. assert (H := CPToSSOKAux cp cp' e s HEq Hmem). unfold InCP in H. apply H; assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets