proposition: Lemma max_ge_b (a b: A): le a b <-> max a b = b.
proof: Proof. unfold max; rewrite le_lt_eq, <- compare_lt_iff, <- compare_eq_iff. split; intro H. - now destruct H as [-> | ->]. - pose proof (comparable_comp_spec a b) as [Hab | Hab | Hab]. + now right. + now left. + exfalso. apply compare_gt_iff in Hab. rewrite Hab in H. subst. now apply compare_gt_irrefl in Hab. Qed.
imports: Coq(Relations RelationClasses Setoid)