∀ {α : Type u_1} (x : Batteries.RBNode α),
  x.min? =
    match x with
    | Batteries.RBNode.nil => none
    | Batteries.RBNode.node c Batteries.RBNode.nil v r => some v
    | Batteries.RBNode.node c l v r => l.min?