Coq中split_string函数实现与无信息丢失证明求助

我在Coq中实现了split_string函数，该函数接收list ascii类型的字符串与f: ascii->bool类型的函数，会在f返回true的ASCII字符处分割字符串，并将分隔符保留为长度1的list ascii字符串。

问题1：Coq标准库是否存在该函数？ #

因未找到对应库函数，自行实现了如下代码：

Fixpoint split_string (f: ascii->bool) (z s: list ascii): list (list ascii) :=
match s with
| [] => [rev z]
| h::t => match f h with
  | true => ([rev z]++[[h]])++(split_string f [] t)
  | false => (split_string f (h::z) t)
  end
end.

调用时需传入空的z参数，例如：

Compute split_string isWhite [] some_string.

问题2：证明输出扁平化后与原输入相等 #

需要证明该函数的输出经concat扁平化后与原输入相等（无信息丢失），已提出定理：

Theorem not_more_not_less_splitWhite: forall (s: list ascii),
s = concat (split_string isWhite [] s).

使用归纳法证明时，处理非空白字符后z不再为空，无法应用归纳假设，目前证明进度如下：

Proof. intros s. induction s.
- simpl. reflexivity.
- simpl. destruct isWhite eqn:W.
   * simpl. rewrite <- IHs. reflexivity.
   * 

若标准库无对应函数，请求指导如何完成证明，或提供更优的split_string实现方案。

内容的提问来源于stack exchange，提问作者Leo G.