proposition: Lemma exists_least_coinitialP r: (has_least r) <-> (exists2 a, coinitial 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)