proposition: Lemma memCPAuxOK : forall m cp s e, memCPAux m cp s = true -> InCP e cp -> S.mem e s = true.
proof: Proof. induction m. unfold memCPAux. intros cp s e Hmem HIn. unfold InCP in HIn. simpl in *. rewrite andb_true_iff in Hmem. do 2 (elim HIn; clear HIn; intro HIn; try (subst; spliter; auto)). intros cp s e Hmem HIn. apply InCPOK in HIn. elim HIn; clear HIn; intro HIn. subst. simpl in Hmem. rewrite andb_true_iff in Hmem. spliter. auto. apply IHm with (tailCP cp); try assumption. simpl in Hmem. rewrite andb_true_iff in Hmem. spliter. assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets