proposition: Lemma queens_safe3E n : queens_safe3 n = queens_explor n :> M _.
proof: Proof. rewrite /queens_safe3 /queens_explor; bind_ext => x. bind_ext => y. rewrite 3!bindA. bind_ext; case. rewrite !bindA. by under [RHS]eq_bind do rewrite bindA. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib