proposition: Lemma finite_set_maximal1 U: sub U (substrate r) -> nonempty U -> exists2 x, inc x U & (forall y, inc y U -> gle r x y -> x = y).
proof: Proof. move: Exercise4_7b=> or Usr neU. set r':= induced_order r U. move: (iorder_osr or Usr) => [or' sr']. move:(sub_finite_set Usr fs); rewrite - sr' => fsE. rewrite - sr' in neU. move: (finite_set_maximal or' fsE neU) => [x [xs xm]]. ex_tac; move=> y yser' xy; symmetry; apply: xm; apply /iorder_gle0P => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)