proposition: Lemma finite_set_maximal r: order r -> finite_set (substrate r) -> nonempty (substrate r) -> exists x, maximal r x.
proof: Proof. move=> or fse nes; apply: Zorn_lemma=>//. move => X Xsr toX. case: (emptyset_dichot X)=> xe. rewrite xe;move: nes=> [z zE]; exists z; split=>//; move=> y; case; case. set (s:= induced_order r X) in toX. have sr: (substrate s = X) by rewrite iorder_sr. have fs: (finite_set (substrate s)). by rewrite sr; apply: (sub_finite_set Xsr fse). have nse: (nonempty (substrate s)) by rewrite sr. move: (finite_set_torder_greatest toX fs nse)=> [x [xsr xge]]. rewrite - sr in Xsr. rewrite - sr; exists x; split; first by apply: Xsr. move=> y yX; exact (iorder_gle1 (xge _ yX)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)