proposition: Lemma singleton_bounded x r: singletonp x -> order r -> sub x (substrate r) -> bounded_both r x.
proof: Proof. move=> [y yp] or xsr. have ysr: inc y (substrate r) by apply: xsr;rewrite yp; fprops. have yy: gle r y y by order_tac. by split; exists y; split=>//; rewrite yp; move=> z /set1_P=> ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)