proposition: Lemma find_one_correct g : size g = hw * hw -> if find_one g is some g1 then refine g g1 /\ sudoku g1 else forall g1, refine g g1 -> ~ sudoku g1.
proof: Proof. move=> Hs. case: find_one (find_one_correct_aux Hs) => [s1|/eqP He s1 Hr Hsu]. by rewrite mem_find_all // => /andP[]. have := mem_find_all s1 Hs. by rewrite Hr Hsu He in_nil. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)