proposition: Lemma index_pmap_inj_mem (s : seq A) (f : A -> option B) a1 a2 b1 b2 : {in s &, injective f} -> a1 \in s -> a2 \in s -> f a1 = Some b1 -> f a2 = Some b2 -> index b1 (pmap f s) < index b2 (pmap f s) <-> index a1 s < index a2 s.
proof: Proof. move=>Inj A1 A2 E1 E2. elim: s Inj A1 A2=>[|k s IH] //= Inj; rewrite /oapp !inE !(eq_sym k). case: eqP Inj=>[<-{k} /= Inj _|]. - rewrite E1 /= !eqxx eq_sym. case: eqP E1 E2=>[->-> [->]|]; first by rewrite eqxx. case: eqP=>[-> Na <- E /= A2|//]. by move/Inj: E Na=>-> //; rewrite inE ?(eqxx,A2,orbT). case eqP=>[<-{k} Na Inj /= A1 _|]; first by rewrite E2 /= eqxx !ltn0. move=>N2 N1 Inj /= A1 A2. have Inj1 : {in s &, injective f}. - by move=>x y X Y; apply: Inj; rewrite inE ?X ?Y ?orbT. case E : (f k)=>[b|] /=; last by rewrite IH. case: eqP E1 E=>[-> <- E|_ _]. - by move/Inj: E N1=>-> //; rewrite inE ?(eqxx,A1,orbT). case: eqP E2=>[-><- E|_ _ _]; last by rewrite IH. by move/Inj: E N2=>-> //; rewrite inE ?(eqxx,A2,orbT). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)