proposition: Lemma concat_in m1 m2 y : y ∈ (concat m1 m2) <-> y ∈ m1 \/ y ∈ m2.
proof: Proof. functional induction (concat m1 m2); intros; try factornode m1. - intuition_in. - intuition_in. - factor_remove_min m2 R. rewrite join_in, (remove_min_in R); simpl; intuition. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)