proposition: Lemma index_pmap_inj (s : seq A) (f : A -> option B) a1 a2 b1 b2 : 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; elim: s=>[|k s IH] //=; rewrite /oapp. case: eqP=>[->{k}|]. - rewrite E1 /= eqxx. case: (a1 =P a2) E1 E2=>[-> -> [/eqP ->] //|]. by case: (b1 =P b2)=>[-> Na <- /Inj /esym/Na|]. case: eqP=>[->{k} Na|N2 N1]; first by rewrite E2 /= eqxx !ltn0. case E : (f k)=>[b|] //=. case: eqP E1 E=>[-><- /Inj/N1 //|_ _]. by case: eqP E2=>[-><- /Inj/N2 //|_ _ _]; rewrite IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)