proposition: Lemma the_greatest_pr2 x: greatest r x -> the_greatest r = x.
proof: Proof. move=> le. have exu: has_greatest r by exists x. exact: (unique_greatest (the_greatest_pr exu) le). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)