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