proposition: Lemma finite_set_torder_wor r: total_order r -> finite_set (substrate r) -> worder r.
proof: Proof. move=> tor fse; move: (tor)=> [or _]. split=>// z zs zne. apply: finite_subset_torder_least =>//. apply: (sub_finite_set zs fse). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)