proposition: Lemma Ex4_11_minR_pr R: (forall x, inc x R -> finite_set x) -> (forall x, inc x R -> exists2 y, sub y x & inc y (min_incl_r R)).
proof: Proof. move => h x xr. case: (inc_or_not emptyset R) => eR. exists emptyset;fprops;apply: Zo_i => // t tr te. apply: extensionality => //; fprops. set n := cardinal x. have nN: inc n Nat by apply /NatP; apply: h. have cxn: cardinal x <=c n by rewrite -/n; fprops. set B := Zo R (fun z => sub z x). pose prop k := exists2 x, inc x B & cardinal x <=c k. have pc: prop n by exists x => //; apply: Zo_i. case: (least_int_prop2 nN pc). move => [y yN cy]; move: (cle0 cy) => cy1. move: (card_nonempty cy1) => ye. by move: yN => /Zo_P; rewrite ye; move => []. set k := cpred; move => [kN [y /Zo_P [yR yx] ck] npk]. exists y=> //; apply: Zo_i => // => z zR zy. symmetry;ex_middle yz. case: npk; exists z; first by apply: Zo_i=> //; apply: (sub_trans zy yx). apply / (cltSleP kN); apply: clt_leT ck. by move/ (strict_sub_smaller):(h _ yR); apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)