proposition: Lemma lt_trans: forall s s' s'', lt s s' -> lt s' s'' -> lt s s''.
proof: Proof. unfold lt. intros a b c. assert (H := ct_compare_fun a b c). inversion_clear H; trivial; intros; discriminate. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface