proposition: Lemma compare_trans (a b c: A) (comp_res: comparison): compare a b = comp_res -> compare b c = comp_res -> compare a c = comp_res.
proof: Proof. destruct comp_res. - apply compare_eq_trans. - apply compare_lt_trans. - apply compare_gt_trans. Qed.
imports: Coq(Relations RelationClasses Setoid)