proposition: Lemma compare_lt_trans (a b c: A): compare a b = Lt -> compare b c = Lt -> compare a c = Lt.
proof: Proof. intros Hab Hbc. apply compare_lt_iff in Hab, Hbc; apply compare_lt_iff. now transitivity b. Qed.
imports: Coq(Relations RelationClasses Setoid)