proposition: Lemma last_filter_Some P `{!∀ x : A, Decision (P x)} l x : last (filter P l) = Some x → ∃ l1 l2, l = l1 ++ x :: l2 ∧ Forall (λ z, ¬P z) l2.
proof: Proof. rewrite <-(reverse_involutive (filter P l)), last_reverse, <-filter_reverse. intros (l1&l2&Heq&Hl)%head_filter_Some. exists (reverse l2), (reverse l1). rewrite <-(reverse_involutive l), Heq, reverse_app, reverse_cons, <-(assoc_L (++)). split; [done|by apply Forall_reverse]. Qed.
imports: stdpp(options)