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