proposition: Lemma queens_explorE n : queens_explor n = queens_state_nondeter n.
proof: Proof. rewrite /queens_explor /queens_state_nondeter. bind_ext => x. bind_ext => y. rewrite 2!bindA. bind_ext => z. rewrite 2!bindA. bind_ext => u. rewrite guardsC; last exact: bindmfail. rewrite 2!bindA. by under eq_bind do rewrite assertE bindA bindretf. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib