proposition: Lemma Exercise2_2b r: order r -> exists x, [/\ sub x (substrate r), worder (induced_order r x) & forall z, upper_bound r x z -> inc z x].
proof: Proof. move=> or; move: (Exercise2_2a or). set B:= Zo (\Po _) _. set ss_order := Zo _ _. move => [[sso sss] iss]. move: (Zorn_lemma sso iss)=> [a [ais am]]. move:(ais); rewrite sss => /Zo_P [] /setP_P asr woia. exists a; split => // z [zsr zu]. set (y:= a +s1 z). have zy: inc z y by rewrite /y;fprops. rewrite -(am y) //. have ysr: (sub y (substrate r)). move=> t /setU1_P; case ; [apply: asr| by move => ->]. apply: Zo_i. move: (iorder_osr or ysr) => [pr1 sr1]. apply /setXp_P;split => //;first (by ue); apply: Zo_i;first by apply /setP_P. split => //; rewrite sr1 => x xy nex. set (t:= x \cap a). have Ha: sub t a by apply: subsetI2r. have Hb: sub t y. by apply: (@sub_trans x) => //; apply: subsetI2l. have Hc: sub t (substrate r) by apply: (@sub_trans y). have Hd: sub x (substrate r) by apply: (@sub_trans y). rewrite iorder_trans //. case: (emptyset_dichot t) => te. have xs: (forall u, inc u x -> u = z). move=> u ux; move: (xy _ ux); case /setU1_P => //. by move=> ua; empty_tac1 u; apply: setI2_i. move: nex => [w wx]; move: (xs _ wx) => wz. exists w; red; rewrite iorder_sr //;split => //. move => // v vx; apply /iorder_gleP;split => //; rewrite (xs _ vx) - wz. by order_tac; apply: Hd. move: woia => [_]; rewrite iorder_sr //; move=> h; move: (h _ Ha te) => [w]. rewrite iorder_trans //; move=> []; rewrite iorder_sr//;move=> ws wl;exists w. have wx: inc w x by apply: (@setI2_1 x a). red; rewrite iorder_sr//;split => // v vx; apply /iorder_gle0P=> //. move: (xy _ vx); case /setU1_P => //. move=> va; exact: (iorder_gle1 (wl _ (setI2_i vx va))). move => ->; exact: (zu _ (Ha _ ws)). aw;split; first by rewrite iorder_sr//; move=> t; rewrite /y; fprops. move=> u v xa h; move: (iorder_gle3 h)(iorder_gle1 h) => [vy uy] vu. move: vy; case /setU2_P => // /set1_P vz. move: (zu _ xa); rewrite -vz => uz. by rewrite (order_antisymmetry or vu uz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)