proposition: Lemma Exercise4_11c M x: max_pure A R M -> inc x (A -s M) -> exists !z, [/\ inc z (\Po A), sub z M & inc (z +s1 x) R].
proof: Proof. move: mnr => [q1 q2 q3 q4]. move => [pm1 pm2 mpx] /setC_P [xA nxm]. apply /unique_existence; split; last first. move => a b [aA aM saR] [bA bM sbR]. ex_middle nab. have ne1: ~ inc x a by move => xa; case: nxm; apply: aM. have ne2: ~ inc x b by move => xa; case: nxm; apply: bM. have ne3: (a +s1 x) <> (b +s1 x). move => eta; case: nab. by rewrite - (setU1_K ne1) - (setU1_K ne2) eta. have xc: inc x ((a +s1 x) \cap (b +s1 x)) by fprops. move: (q3 _ _ saR sbR ne3 _ xc); move => [Z [Zr sz nxz]]. have zM: sub Z M. move => t tZ; move: (sz _ tZ); case /setU2_P; case /setU1_P; fprops; by move => tx; case: nxz; rewrite - tx. by case: (pm2 _ zM). have ta: sub (M +s1 x) A by move => t; case /setU1_P; [ fprops | by move => ->]. have [t ts tr]: exists2 t, sub t (M +s1 x) & inc t R. case: (p_or_not_p (pure R (M +s1 x))) => npt. case: nxm; rewrite (mpx _ npt (@sub_setU1 M x) ta); fprops. by ex_middle bad; case: npt => s ts b3;case: bad; exists s. move: (sub_trans ts ta) => tA. set z := t -s1 x. have zM: sub z M. move => s /setC1_P [td te]. by move: (ts _ td); case /setU1_P. move: (pm2 _ zM) => zR. have zt: sub z t by move => u /setC1_P []. case: (inc_or_not x t) => xy. move: (setC1_K xy) => tc. exists z;split => //; first by (apply /setP_P; apply: (sub_trans zt tA)). by rewrite /z tc. case: zR; have -> //: z = t. set_extens s; first by move /setC1_P => []. by move => st; apply /setC1_P;split => //; dneg sx; rewrite - sx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)