proposition: Lemma corollary45 s : assert (safeAcc_scanl 0 [::] [::]) s = protect (put (0%Z, [::], [::]) >> foldr opdot_queens (Ret [::]) s).
proof: Proof. rewrite assert_all_scanl. rewrite /protect; bind_ext => st. rewrite 3!bindA. bind_ext; case. by rewrite -theorem44 bindA. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib