fact: Fixpoint splits_bseq s : M ((size s).-bseq A * (size s).-bseq A)%type := if s isn't x :: xs then Ret ([bseq of [::]], [bseq of [::]]) else splits_bseq xs >>= (fun '(ys, zs) => Ret ([bseq of x :: ys], widen_bseq (leqnSn _) zs) [~] Ret (widen_bseq (leqnSn _) ys, [bseq of x :: zs])).
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)