proposition: Theorem find_one_correct: forall s, length s = size * size -> match find_one s with None => forall s1, refine s s1 -> ~ sudoku s1 | Some s1 => refine s s1 /\ sudoku s1 end.
proof: Proof. intros s Hs; unfold find_one. match goal with |- context [find_one_aux ?X ?Y ?Z] => generalize (find_one_aux_sat X Y Z); case (find_one_aux X Y Z); auto end. intros s1 H; case H; auto with arith; clear H. apply invariant_gen_init_clauses; auto. intros HH s1 H1 H2; case HH with s1; auto. apply invariant_gen_init_clauses; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia