Lean4
/-- O(log n). Insert an element into the set, preserving balance and the BST property.
If an equivalent element is already in the set, this replaces it.
insert 1 {1, 2, 3} = {1, 2, 3}
insert 4 {1, 2, 3} = {1, 2, 3, 4}
Using a preorder on `ℕ × ℕ` that only compares the first coordinate:
insert (1, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 1)}
insert (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2), (3, 1)} -/
protected def insert (x : α) : Ordnode α → Ordnode α
| nil => ι x
| node sz l y r =>
match cmpLE x y with
| Ordering.lt => balanceL (Ordnode.insert x l) y r
| Ordering.eq => node sz l x r
| Ordering.gt => balanceR l y (Ordnode.insert x r)
