proposition: Lemma lt_not_eq: forall s s', lt s s' -> ~ eq s s'.
proof: Proof. unfold lt, eq. intros s s' H H'. rewrite equal_spec, <- compare_equal in H'. congruence. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface