proposition: Lemma compare_eq_trans (a b c: A): compare a b = Eq -> compare b c = Eq -> compare a c = Eq.
proof: Proof. intros Hab Hbc. apply compare_eq_iff in Hab, Hbc; apply compare_eq_iff. now subst. Qed.
imports: Coq(Relations RelationClasses Setoid)