proposition: Lemma qperm_cons_rcons h (t : seq A) : qperm (h :: t) = qperm (rcons t h) :> M _.
proof: Proof. by apply: perm_eq_qperm; rewrite perm_sym perm_rcons perm_refl. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)