proposition: Lemma find_just_one_correct g : size g = hw * hw -> match find_just_one g with jNone => forall g1, refine g g1 -> ~ sudoku g1 | jOne g1 => [/\ refine g g1, sudoku g1 & forall g2, refine g g2 -> sudoku g2 -> g1 = g2] | jMore g1 g2 => [/\ refine g g1, sudoku g1, refine g g2, sudoku g2 & g1 != g2] end.
proof: Proof. move=> Hs. case: find_just_one (find_just_one_correct_aux Hs) => [H g1 Hr Hsu||]. - by have := mem_find_all g1 Hs; rewrite Hr Hsu H in_nil. - move=> g1 He. have: g1 \in find_all g by rewrite He in_cons eqxx. rewrite mem_find_all // => /andP[Hs1 Hr1]. split => // g2 Hs2 Hr2. have: g2 \in find_all g by rewrite mem_find_all // Hs2. by rewrite He inE => /eqP. move=> g1 g2. rewrite !mem_find_all // => [] [/andP[H1 H2] /andP[H3 H4] H5]. by split. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)