mathlib

ed989ff5 - feat(data/tree): Add definitions about binary trees; special support for `tree unit` (#16715)

feat(data/tree): Add definitions about binary trees; special support for `tree unit` (#16715) Provide convenience API for `tree unit`. In particular, define a recursor for `tree unit` as well as other helper lemmas. In addition, define common functions on binary trees such as `nodes`, `num_leaves`, `height`, and prove basic lemmas about these functions, such as the fact that the number of leaves is one more than the number of internal nodes and the height is at most the number of nodes. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>