proposition: Lemma compare_trans : forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
proof: Proof. intros c x y z. destruct c; unfold compare; do 2 (destruct O.compare; intros; try discriminate); elim_comp; auto. Qed.
imports: OrderedType