proposition: Lemma gmerge_gt m m' x `{!Ok m, !Ok m'} : x < m -> x < m' -> x < gmerge m m'.
proof: Proof. intros ? ? y Hy. apply gmerge_in in Hy; intuition_in; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)