proposition: Lemma split_first (A : eqType) (l : seq A) (P : pred A) : ~~ all [predC P] l -> {bl1l2 : (A * seq A * seq A) | [/\ all [predC P] bl1l2.1.2, P bl1l2.1.1 & l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}.
proof: Proof. elim: l => //= b l IH. rewrite negb_and negbK; case: (boolP (b \in P)) => [bIP _| bNIP /= /IH [[[c l1] l2] [H1 H2 ->]]]. by exists (b, [::], l); split. by exists (c, b :: l1, l2); split; rewrite /= ?bNIP. Qed.
imports: mathcomp(all_ssreflect finmap)