proposition: Theorem init_c_sudoku: forall s, length s = size * size -> (sat init_c s <-> sudoku s).
proof: Proof. Proof with auto. generalize (ref_list_ulist); intros Eq1. generalize (ref_list_length); intros Eq2. intros s H; case (init_c_sat s); auto; intros HH0 HH1; split; intros H1. case HH0; clear HH0 HH1; auto; intros HH0 (HH1, (HH2, HH3)); unfold sudoku . split... repeat split; intros i U; apply Permutation_sym; apply ulist_eq_permutation... rewrite length_row... rewrite length_column... rewrite length_rect... apply HH1; clear HH0 HH1. case H1; clear H1; intros H0 (H1, (H2, H3)). repeat split; try (intros i Hi j Hj; apply Permutation_in with (2 := Hj); try apply Permutation_sym; auto). intros (x, y) (HH1, HH2). apply Permutation_in with (row x s)... rewrite get_row; try apply nth_In; try rewrite length_row... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia