proposition: Lemma sudokuP g : reflect [/\ 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] (sudoku g).
proof: Proof. apply: (iffP and4P) => [] [H1 H2 H3 H4]; split; auto. - by apply/eqP. - by move=> i iLhw; have /forallP := H2 => /(_ (Ordinal iLhw)). - by move=> i iLhw; have /forallP := H3 => /(_ (Ordinal iLhw)). - by move=> i iLhw; have /forallP := H4 => /(_ (Ordinal iLhw)). - by apply/eqP. - by apply/forallP => i; apply H2. - by apply/forallP => i; apply H3. by apply/forallP => i; apply H4. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)