proposition: Lemma finite_set_torder_least r: total_order r -> finite_set (substrate r) -> nonempty (substrate r) -> has_least r.
proof: Proof. move=> tor fss nes; move: (tor)=> [or _]. rewrite - (iorder_substrate or). apply: finite_subset_torder_least; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)