proposition: Lemma index_last_sub (p1 p2 : pred A) x (s : seq A) : subpred p1 p2 -> uniq (x :: s) -> index (last x (filter p1 s)) (x :: s) <= index (last x (filter p2 s)) (x :: s).
proof: Proof. move=>S; elim: s x=>[|k s IH] //= x; rewrite !inE negb_or -andbA. rewrite -(eq_sym k) -!(eq_sym (last _ _)); case/and4P=>N Sx Sk U. have [Ux Uk] : uniq (x :: s) /\ uniq (k :: s) by rewrite /= Sx Sk U. case P1 : (p1 k)=>/=. - rewrite (S _ P1) /=; case: (last k _ =P k). - move/last_nochange; rewrite mem_filter (negbTE Sk) andbF /=. move/eqP=>-> /=; rewrite (negbTE N). case: (last k _ =P k); first by move=>->; rewrite (negbTE N). by case/eqP/last_filter_change/andP; case: eqP Sx=>// <- /negbTE ->. move/eqP=>N1; move: (last_filter_neq S Sk N1)=>N2. move: (IH _ Uk); rewrite /= !(eq_sym k). rewrite (negbTE N1) (negbTE N2) -(last_changeE1 N1 x) -(last_changeE1 N2 x). rewrite (negbTE (last_changeE2 N1 _)) ?(mem_filter,negb_and,Sx,orbT) //. by rewrite (negbTE (last_changeE2 N2 _)) ?(mem_filter,negb_and,Sx,orbT). case P2 : (p2 k)=>/=. - case: (last x _ =P x)=>// /eqP N1; move: (last_filter_neq S Sx N1)=>N2. move: (IH _ Ux); rewrite /= !(eq_sym x) (negbTE N1) (negbTE N2). rewrite -(last_changeE1 N1 k) {1 3}(last_changeE1 N2 k). rewrite (negbTE (last_changeE2 N1 _)) ?(mem_filter,negb_and,Sk,orbT) //. by rewrite !(negbTE (last_changeE2 N2 _)) ?(mem_filter,negb_and,Sk,Sx,orbT). case: (last x _ =P x)=>// /eqP N1; move: (last_filter_neq S Sx N1)=>N2. move: (IH _ Ux); rewrite /= !(eq_sym x) (negbTE N1) (negbTE N2). rewrite -(last_changeE1 N1 k) -(last_changeE1 N2 k). rewrite (negbTE (last_changeE2 N1 _)) ?(mem_filter,negb_and,Sk,orbT) //. by rewrite !(negbTE (last_changeE2 N2 _)) ?(mem_filter,negb_and,Sk,orbT). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)