proposition: Lemma indexlast_mask (s : seq A) m a b : uniq s -> a \in mask m s -> b \in mask m s -> indexlast a (mask m s) < indexlast b (mask m s) <-> indexlast a s < indexlast b s.
proof: Proof. elim: m s=>[|x m IH][|k s] //= /andP [K U]; case: x=>[|Ma Mb] /=; rewrite !indexlast_cons. - rewrite !inE; case/orP=>[/eqP Ea|Ma]. - rewrite -{k}Ea in K *. have Km: (a \notin mask m s) by apply: contra K; apply: mem_mask. case/orP=>[/eqP ->|]; rewrite eqxx /=; first by rewrite K ltnn. case: eqP=>[->|Nab] H /=; first by rewrite !ltnn. by rewrite K Km. case/orP=>[/eqP Eb|Mb]. - rewrite -{k}Eb in K *. have ->: (b \notin mask m s) by apply: contra K; apply: mem_mask. by rewrite eqxx /= K. rewrite Ma Mb (mem_mask Ma) (mem_mask Mb) /= !andbF. by apply: 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)