proposition: Lemma index_mask (s : seq A) m a b : uniq s -> a \in mask m s -> b \in mask m s -> index a (mask m s) < index b (mask m s) <-> index a s < index b s.
proof: Proof. elim: m s=>[|x m IH][|k s] //= /andP [K U]; case: x=>[|Ma Mb] /=. - rewrite !inE; case/orP=>[/eqP <-|Ma]. - by case/orP=>[/eqP ->|]; rewrite eqxx //; case: eqP. case/orP=>[/eqP ->|Mb]; first by rewrite eqxx. by case: eqP; case: eqP=>//; rewrite ltnS IH. case: eqP Ma K=>[-> /mem_mask -> //|Ka]. case: eqP Mb=>[-> /mem_mask -> //|Kb Mb Ma]. by rewrite ltnS IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)