proposition: Lemma qperm_slowsort : (qperm >=> slowsort) = slowsort :> (seq T -> M (seq T)).
proof: Proof. by rewrite /slowsort -kleisliA qperm_idempotent. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)