proposition: Lemma exists_greatest_cofinalP r: (has_greatest r) <-> (exists2 a, cofinal r a & singletonp a).
proof: Proof. split. move=> [a [asr h]]; exists (singleton a); last by exists a. split; [by move=> t /set1_P -> | move=> x xr; exists a;fprops]. move=> [a [asr h] [b bp]];exists b;split. apply: asr; rewrite bp; fprops. by move=> x xsr; move:(h _ xsr)=> [y]; rewrite bp; move /set1_P => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)