proposition: Lemma above_trans {elt} (m:t elt) x y : x < y -> m < x -> m < y.
proof: Proof. intros until 3; order. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)