fact: Definition sudoku g := [&& size g == hw * hw, [forall i : 'I_hw, perm_eq (row i g) sref], [forall i : 'I_hw, perm_eq (column i g) sref] & [forall i : 'I_hw, perm_eq (rect i g) sref]].
imports: mathcomp(all_ssreflect) mathcomp(zify)