proposition: Lemma qperm_preserves_elements (A : eqType) (s : seq A) : qperm s = qperm s >>= (fun x => guard (perm_eq x s) >> Ret x) :> M _.
proof: Proof. have [n ns] := ubnP (size s); elim: n s ns => // n ih s ns. move: s ns => [ns |h t]. by rewrite qperm_nil bindretf perm_refl guardT bindskipf. rewrite /= ltnS => ns; rewrite qperm_cons bindA splits_guard_subseq !bindA. bind_ext => -[a b]; rewrite /= !bindA; apply: bind_ext_guard => /and3P[_ _ abt]. rewrite !bindretf /liftM2 /= !bindA ih; last first. by rewrite (leq_trans _ ns) // ltnS -(perm_size abt) size_cat leq_addr. rewrite !bindA; bind_ext => a'; rewrite !bindA; apply: bind_ext_guard => aa'. rewrite !bindretf !bindA ih; last first. by rewrite (leq_trans _ ns) // ltnS -(perm_size abt) size_cat leq_addl. rewrite !bindA; bind_ext => b'; rewrite !bindA; apply: bind_ext_guard => bb'. rewrite !bindretf -[in X in _ = X >> _]cat_rcons -cats1 -catA perm_catCA. by rewrite perm_cons (perm_trans (perm_cat aa' bb') abt) guardT bindskipf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)