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