proposition: Lemma the_least_pr2 x: least r x -> the_least r = x.
proof: Proof. move=> le. have exu: has_least r by exists x. exact: (unique_least (the_least_pr exu) le). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)