proposition: Lemma gtb_compat : forall x, Proper (E.eq==>Logic.eq) (gtb x).
proof: Proof. red; intros x a b H. generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto. - intros. symmetry; rewrite H1. apply ME.eq_lt with a; auto with ordered_type. rewrite <- H0; auto. - intros. rewrite H0. apply ME.eq_lt with b; auto. rewrite <- H1; auto. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide