fact: Definition dsplits (A : UU0) (s : seq A) : M (dsplitsT A (size s)) := splits s >>= dassert [pred n | size n.1 + size n.2 == size s].
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)