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