proposition: Theorem init_c_ordered: ordered init_c.
proof: Proof. unfold init_c. apply fold_clause_insert_ordered with (f := (fun iz => gen_row (fst iz) (snd iz))); auto. intros; apply gen_row_ordered. apply fold_clause_insert_ordered with (f := (fun iz => gen_column (fst iz) (snd iz))); auto. intros; apply gen_column_ordered. apply fold_clause_insert_ordered with (f := (fun iz => gen_rect (fst iz) (snd iz))); auto. intros; apply gen_rect_ordered. apply all_cell_ordered. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia