fact: Definition queens_ok (i_xus_yds : Z * seq Z * seq Z) := let: (_, xus, yds) := i_xus_yds in match xus, yds with | x :: us, y :: ds => (x \notin us) && (y \notin ds) | _, _ => false end.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib