proposition: Lemma head_filter_Some P `{!∀ x : A, Decision (P x)} l x : head (filter P l) = Some x → ∃ l1 l2, l = l1 ++ x :: l2 ∧ Forall (λ z, ¬P z) l1.
proof: Proof. intros Hl. induction l as [|x' l IH]; [done|]. rewrite filter_cons in Hl. case_decide; simplify_eq/=. - exists [], l. repeat constructor. - destruct IH as (l1&l2&->&?); [done|]. exists (x' :: l1), l2. by repeat constructor. Qed.
imports: stdpp(options)