Theorem: Std.RBNode.max?_mem (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
a : α
t : RBNode α
h : RBNode.max? t = some a
⊢ a ∈ t
Tactic:
simpa using min?_mem ((min?_reverse _).trans h)
State after:
no goals