proposition: Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x.
proof: Proof. intros; rewrite <- compare_gt_iff. unfold gtb. destruct E.compare; intuition; try discriminate. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide