proposition: Lemma in_mask_count x m xs : count_mem x xs <= 1 -> x \in mask m xs = (x \in xs) && nth false m (index x xs).
proof: Proof. elim: xs m => [|y xs IHs] m /=; first by rewrite mask0 in_nil. case: m=>/=[|b m]; first by rewrite in_nil nth_nil andbF. case: b; rewrite !inE eq_sym; case: eqP=>//= _. - by rewrite add0n; apply: IHs. - rewrite -{2}(addn0 1%N) leq_add2l leqn0 => /eqP Hc. rewrite IHs; last by rewrite Hc. by move/count_memPn/negbTE: Hc=>->. by rewrite add0n; apply: IHs. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)