proposition: Lemma gmerge_lt m m' x `{!Ok m, !Ok m'} : m < x -> m' < x -> gmerge m m' < x.
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)