proposition: Lemma memCPConsHd : forall p s x, S.mem p s = true -> memCPAux n x s = true -> memCP (consHeadCP p x) s = true.
proof: Proof. intros p s x Hmem Hmemcp. apply memMemCPOK. intros e HIn. apply InCPOK in HIn. simpl in HIn. elim HIn; clear HIn; intro HIn. subst; assumption. apply memCPAuxOK with n x; assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets