fact: Definition partition_slowsort (xs : seq T) : M (seq T) := if xs isn't h :: t then Ret [::] else let: (ys, zs) := partition h t in liftM2 (fun a b => a ++ h :: b) (slowsort ys) (slowsort zs).
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)