proposition: Lemma singleton_rb x e : Rbt (singleton x e).
proof: Proof. unfold singleton. exists 1; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)