proposition: Lemma join_in l x d r y : y ∈ (join l x d r) <-> y == x \/ y ∈ l \/ y ∈ r.
proof: Proof. join_tac l x d r. - simpl join. rewrite add_in; intuition_in. - rewrite add_in; intuition_in. - rewrite bal_in, Hlr. clear Hlr Hrl. intuition_in. - rewrite bal_in, Hrl. clear Hlr Hrl. intuition_in. - apply create_in. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)