proposition: Lemma split_last (A : eqType) (l : seq A) (P : pred A) : ~~ all [predC P] l -> {bl1l2 | [/\ P bl1l2.1.1, all [predC P] bl1l2.2 & l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}.
proof: Proof. move=> lA. case: (@split_first _ (rev l) P); first by rewrite all_rev. move=> [[b l1] l2] [H1 H2 H3]. exists (b, rev l2, rev l1); split => //; first by rewrite all_rev. by rewrite -{1}[l]revK H3 rev_cat /= rev_cons cat_rcons. Qed.
imports: mathcomp(all_ssreflect finmap)