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