proposition: Lemma compare_gt: forall s s', compare_fun s s' = Gt -> lt s' s.
proof: Proof. unfold lt. intros s s'. rewrite compare_inv. case compare_fun; trivial; intros; discriminate. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface