proposition: Lemma above_iff {elt} x (m:t elt) : m < x <-> above x m = true.
proof: Proof. induction m as [|c l IHl y v r IHr]; simpl. - intuition. apply above_leaf. - rewrite above_node. case K.compare_spec. + split; intros; try easy. intuition. order. + split; intros; try easy. intuition. order. + rewrite andb_true_iff; intuition. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)