proposition: Lemma worder_least r: worder r -> nonempty (substrate r) -> has_least r.
proof: Proof. move=> [or wo] ne. move: (wo _ (@sub_refl (substrate r)) ne)=> [x]. by rewrite iorder_substrate //; exists x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)