proposition: Lemma ltb_tree_iff : forall x s, lt_tree x s <-> ltb_tree x s = true.
proof: Proof. induction s as [|c l IHl y r IHr]; simpl. - unfold lt_tree; intuition_in. - elim_compare x y. + split; intros; try discriminate. assert (X.lt y x) by auto. order. + split; intros; try discriminate. assert (X.lt y x) by auto. order. + rewrite !andb_true_iff, <-IHl, <-IHr. unfold lt_tree; intuition_in; order. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat