proposition: Lemma mu_queensE {M : nondetMonad} n : mu_queens n = perms (map Z_of_nat (iota 0 n)) >>= assert (safeAcc_scanl 0 [::] [::]) :> M _.
proof: Proof. rewrite /mu_queens; bind_ext => s. by rewrite assertE (safeE s) safeAccE -assertE. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib