proposition: Lemma partition_slowsort_spec : partition_slowsort `<.=` slowsort.
proof: Proof. move; elim => [/=|h t ih]. rewrite slowsort_nil; exact: refin_refl. rewrite slowsort_splits. apply: (@refin_trans _ _ (splits t >>= fun yz => assert (is_partition h) yz >>= fun '(ys, zs) => slowsort ys >>= fun ys' : seq T => slowsort zs >>= fun zs' => Ret (ys' ++ h :: zs'))); last first. apply: refin_bindl => -[? ?]. rewrite assertE !bindA bindretf; exact: refin_refl. rewrite -bindA; apply: refin_trans; last exact/refin_bindr/partition_spec. rewrite bindretf /partition_slowsort; 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)