proposition: Lemma bind_slowsort_guard (s : seq E) B (f : seq E -> M B) : (slowsort s >>= f) = slowsort s >>= (fun x => guard (size s == size x) >> f x).
proof: Proof. rewrite -(slowsort_preserves_size2 s (fun a b => guard (size s == b) >> f a)). by rewrite eqxx guardT; under [in RHS]eq_bind do rewrite bindskipf. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)