# Join of a list of lists #

This file proves basic properties of `List.join`

, which concatenates a list of lists. It is defined
in `Init.Data.List.Basic`

.

In a join, taking the first elements up to an index which is the sum of the lengths of the
first `i`

sublists, is the same as taking the join of the first `i`

sublists.

In a join, dropping all the elements up to an index which is the sum of the lengths of the
first `i`

sublists, is the same as taking the join after dropping the first `i`

sublists.

Taking only the first `i+1`

elements in a list, and then dropping the first `i`

ones, one is
left with a list of length `1`

made of the `i`

-th element of the original list.

Taking only the first `i+1`

elements in a list, and then dropping the first `i`

ones, one is
left with a list of length `1`

made of the `i`

-th element of the original list.

In a join of sublists, taking the slice between the indices `A`

and `B - 1`

gives back the
original sublist of index `i`

if `A`

is the sum of the lenghts of sublists of index `< i`

, and
`B`

is the sum of the lengths of sublists of index `≤ i`

.

In a join of sublists, taking the slice between the indices `A`

and `B - 1`

gives back the
original sublist of index `i`

if `A`

is the sum of the lenghts of sublists of index `< i`

, and
`B`

is the sum of the lengths of sublists of index `≤ i`

.

Auxiliary lemma to control elements in a join.

Auxiliary lemma to control elements in a join.

The `n`

-th element in a join of sublists is the `j`

-th element of the `i`

th sublist,
where `n`

can be obtained in terms of `i`

and `j`

by adding the lengths of all the sublists
of index `< i`

, and adding `j`

.

We can rebracket `x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x)`

to
`(x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x`

where `L = [l₁, l₂, ..., lₙ]`

.

Reversing a join is the same as reversing the order of parts and reversing all parts.

Joining a reverse is the same as reversing all parts and reversing the joined result.