proposition: Lemma qsort_spec : Ret \o qsort `<.=` (@slowsort M _ _).
proof: Proof. move=> s /=. apply qsort_elim => [|h t ihys ihzs]. rewrite slowsort_nil; exact: refin_refl. apply: (refin_trans _ (partition_slowsort_spec _)). rewrite /=. move H : (partition h t) => ht. move: ht H => [ys zs] /= pht. rewrite pht in ihys ihzs. apply: (refin_trans _ (refin_liftM2 ihys ihzs)). rewrite liftM2_ret; exact: refin_refl. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)