Type of balanced trees with two custom values (more efficient than a pair)

Leaf constructor, the empty tree

Smart Node constructor, ensuring that the resulting tree is balanced and has the appropriate size.

Cost of node l x r is expected to be O(log |size l - size r|) amortized, i.e proportional to the logarithm of the disbalance. In particular, if l and r are similarly-sized, it operates in constant time on average. NOT PROVEN

User-values can be moved in different subtrees of the result, but the ordering is preserved (so data stay correct if the operation applied on values is associative or the relation expected between them is transitive).

Accessor to the size

Concatenate two trees. Cost of join l r is O(log (min size l size r)). NOT PROVEN

Return the n'th node in tree order