proposition: Lemma compare : forall s s' : t, Compare lt eq s s'.
proof: Proof. intros. case_eq (compare_fun s s'); intro H. - apply EQ. apply compare_eq, H. - apply LT. assumption. - apply GT. apply compare_gt, H. Defined.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface