proposition: Lemma refin_partition_slowsort p s : Ret (partition p s) >>= (fun '(a, b) => slowsort a >>= (fun a' => slowsort b >>= (fun b' => Ret (a' ++ p :: b')))) `<=` (slowsort (p :: s) : M _).
proof: Proof. rewrite slowsort_splits. apply: refin_trans; first exact/refin_bindr/(partition_spec M p s). rewrite bindA; apply: refin_bindl => -[a b]. rewrite assertE (bindA _ (fun _ => Ret (a, b))) bindretf /= bindA. 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)