proposition: Lemma create_in l x e r y : y ∈ (create l x e r) <-> y == x \/ y ∈ l \/ y ∈ r.
proof: Proof. unfold create. intuition_in. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)