proposition: Lemma nonempty_closed_interval r x: order r -> closed_interval r x -> nonempty x.
proof: Proof. move=> or [a [b [asr bsr ab xab]]]. exists a; rewrite xab; apply: Zo_i =>//. by split=>//; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)