proposition: Lemma bind_qperm_guard A (s : seq A) B (f : seq A -> M B) : qperm s >>= f = qperm s >>= (fun x => guard (size s == size x) >> f x).
proof: Proof. rewrite -(qperm_preserves_size2 s (fun a b => guard (size s == b) >> f a)). rewrite eqxx guardT. by under [in RHS]eq_bind do rewrite bindskipf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)