Proof of logarithmic depth for AVL trees?

Stream: Is there code for X?

[Dessertion]

Is there code currently available that formalizes the balancing properties for AVL trees (or other well-known balanced BSTs)? I see that Batteries has an RBMap module with accompanying lemmas for Red-Black trees; are there similar libraries out there?

[Markus Himmel]

Lean core merged an implementation of weight-balanced trees today which contains (pretty hairy) proofs about balancing, see here.

[Dessertion]

Wow, that's some incredible timing on my part then! Thanks!