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