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