proposition: Lemma least_and_greatest x: least r x -> greatest r x -> singletonp (substrate r).
proof: Proof. move => [xs lex][_ gex]; exists x. apply: (set1_pr xs) => z zs; move: (lex _ zs)(gex _ zs)=> xy yx. order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)