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; rewrite ?compare_Eq, ?compare_Lt, ?compare_Gt; transitivity y; auto. Qed.
imports: OrderedType Orders