proposition: Lemma rbal_find l x v r `{!Ok l, !Ok r} : l < x -> x < r -> rbal l x v r === Rd l x v r.
proof: Proof. intros Hl Hr y. apply find_mapsto_equiv; auto using rbal_mapsto; autok. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)