proposition: Lemma finite_set_minimal1 U: sub U (substrate r) -> nonempty U -> exists2 x, inc x U & (forall y, inc y U -> gle r y x -> y = x).
proof: Proof. move: Exercise4_7b => or Usr neU. set r':= opp_order (induced_order r U). move: (iorder_osr or Usr) => [or1 sr1]. move: (opp_osr or1) => [or']; rewrite sr1 => 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; apply: xm; apply /opp_gleP. apply /iorder_gle0P => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)