proposition: Lemma above_node {elt} x h l y (e:elt) r : Node h l y e r < x <-> l < x /\ y < x /\ r < x.
proof: Proof. apply allkeys_node with (P := fun z => z < x). now intros ? ? ->. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)