proposition: Lemma compare : forall x y : t, OrderedType.Compare lt eq x y.
proof: Proof. intros x y. assert (H := (O.compare_spec x y)). destruct (O.compare x y). - constructor 2. now inversion H. - constructor 1. now inversion H. - constructor 3. now inversion H. Qed.
imports: SetoidList Orders