proposition: Lemma apart_node_r {elt} h l x v r (m:t elt) : m < (Node h l x v r) <-> m < l /\ m < x /\ m < r.
proof: Proof. unfold "<"; unfold lt_map_map, lt_map_key, AllKeys. setoid_rewrite below_node. split; [ | intuition]. intros H; repeat split; intros y IN; now specialize (H y IN). Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)