proposition: Lemma find_one_aux_correct st g st1 : if find_one_aux st g st1 is some g1 then g1 \in find_all_aux st g st1 else find_all_aux st g st1 == [::].
proof: Proof. elim: st g st1=> [s [|[[n p] v]]|[[n p] v] st IH g [|[[n1 p1] v1] st1]] //=. - by rewrite in_cons eqxx. - by rewrite in_cons eqxx. elim: behead p1 1 g st1 => //= [] [] bs IH1 p1 k g st1. case: find_one_aux (IH (update p1 k g) (update_anti_literals p1 k st1)). by move=> s1 s1If; rewrite mem_merge_sudoku mem_cat s1If. move/eqP=> ->. case: try_one (IH1 p1 k.+1 g st1) => [s1|/eqP->//]. by rewrite mem_merge_sudoku => ->. by apply: IH1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)