proposition: Lemma leb_1 : forall x y, leb x y = true <-> ~E.lt y x.
proof: Proof. intros; unfold leb, gtb; destruct (E.compare x y); intuition try discriminate; ME.order. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide