proposition: Theorem gen_column_sat: forall j z s, length s = size * size -> j < size -> (clause_sat (gen_column j z) s <-> In z (column j s)).
proof: Proof. intros j z s H H0. assert (Eq1: length (column j s) = size); try apply length_column; auto. split. intros (l, (H1, H2)). case (gen_column_correct l j z); intros tmp _; case tmp; auto; clear tmp. intros i (H3, H4). case (in_ex_nth _ z 0 (column j s)); intros _ tmp; apply tmp; clear tmp. subst; exists i; split; auto. rewrite Eq1; auto. rewrite <- get_column; auto. intros H1. case (in_ex_nth _ z 0 (column j s)); intros tmp _; case tmp; auto; clear tmp. intros i (H2, H3). rewrite <- get_column in H3; auto. exists (L (Pos i j) z); split; auto. case (gen_column_correct (L (Pos i j) z) j z); intros _ tmp; apply tmp; clear tmp. exists i; split; auto. rewrite <- Eq1; auto. red; apply sym_equal; auto. rewrite Eq1 in H2; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia