proposition: Lemma lt_not_eq : forall s s', lt s s' -> ~ eq s s'.
proof: Proof. unfold lt, eq. intros s s' Hlt Heq. rewrite Heq in Hlt. apply (StrictOrder_Irreflexive s'); auto. Qed.
imports: FSetInterface FSetFacts MSetInterface MSetFacts