mathlib3 documentation

data.rbtree.default_lt