proposition: Lemma index_pmap_inj_in (s : seq A) (f : A -> option B) a1 a2 b1 b2 : {in s & predT, injective f} -> 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 E1 E2. case A1 : (a1 \in s); last first. - move/negbT/index_sizeE: (A1)=>->. suff /index_sizeE -> : b1 \notin pmap f s by rewrite !ltnNge !index_size. rewrite mem_pmap; apply/mapP; case=>x X /esym; rewrite -E1=>E. by move/(Inj _ _ X): E A1=><- //; rewrite X. case A2 : (a2 \in s). - by apply: index_pmap_inj_mem=>// x y X _; apply: Inj. move/negbT/index_sizeE: (A2)=>->. suff /index_sizeE -> : b2 \notin pmap f s. - by rewrite !index_mem /= A1 mem_pmap; split=>// _; apply/mapP; exists a1. rewrite mem_pmap; apply/mapP; case=>x X /esym; rewrite -E2=>E. by move/(Inj _ _ X): E A2=><- //; rewrite X. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)