proposition: Lemma slowsort_cons p xs : slowsort (p :: xs) = splits xs >>= (fun '(ys, zs) => qperm ys >>= (fun ys' => qperm zs >>= (fun zs' => assert sorted (ys' ++ p :: zs')))).
proof: Proof. rewrite /slowsort kleisliE qperm_cons bindA. by bind_ext => -[a b]; rewrite liftM2E. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)