proposition: Lemma the_greatest_pr: has_greatest r -> greatest r (the_greatest r).
proof: Proof. rewrite /the_greatest=> h; apply: (proj1(select_pr _ _)). by move: h => [z zl]; exists z => //; move: zl => [ok _]. by move => x y xsr xlt ysr ylt; apply: unique_greatest. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)