proposition: Theorem invariant_init_c: forall s, length s = size * size -> empty s -> invariant init_c s.
proof: Proof. intros s Hs Hs1. split; auto. apply init_c_ordered. split; auto. apply valid_init_c; auto. split; auto. intros s1 (_, (Hs2, _)). generalize (init_c_sat s1 Hs2); intros Hs3. generalize ref_list_ulist; intros F0. generalize ref_list_length; intros F1. apply iff_sym; apply iff_trans with (1 := Hs3); clear Hs3. split; intros (V1, (V2, (V3, V4))); repeat split; auto. intros; apply Permutation_sym; apply ulist_eq_permutation; auto. rewrite length_row; auto. intros; apply Permutation_sym; apply ulist_eq_permutation; auto. rewrite length_column; auto. intros; apply Permutation_sym; apply ulist_eq_permutation; auto. rewrite length_rect; auto. intros i Hi x Hx; apply Permutation_in with ref_list; auto; apply Permutation_sym; auto. intros i Hi x Hx; apply Permutation_in with ref_list; auto; apply Permutation_sym; auto. intros i Hi x Hx; apply Permutation_in with ref_list; auto; apply Permutation_sym; auto. intros (x, y) (Hx, Hy); apply Permutation_in with (row x s1); auto. case (in_ex_nth _ (get (Pos x y) s1) out (row x s1)). intros _ tmp; apply tmp; clear tmp; auto. exists y; split; auto. rewrite length_row; auto. unfold get, row; simpl. rewrite jump_add; rewrite <- jump_nth. apply sym_equal; apply take_nth; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia