proposition: Lemma find_last_last: forall l p el, nth_error l p = Some el -> P el -> exists q, find_last l = Some q /\ q >= p.
proof: Proof. induction l; intros. destruct p; inversion H. destruct p. inversion H. simpl; destruct (P_dec el). destruct (find_last l). exists (S n); split; [trivial | lia]. exists 0; split; [trivial | lia]. absurd (P el); trivial. destruct (IHl p el) as [w [lw wp]]; trivial. exists (S w); split. simpl; rewrite lw; trivial. lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)