proposition: Lemma qperm_rcons (s : seq A) x : qperm (rcons s x) = qperm s >>= (fun s' => qperm (rcons s' x)) :> M _.
proof: Proof. by rewrite -iperm_qperm iperm_rcons_bind. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)