proposition: Lemma Exercise4_11e M x: max_pure A R M -> inc x (A -s M) -> inc (Ex4_11EM M x +s1 x) (min_incl_r R).
proof: Proof. move => mm xa. move: (Exercise4_11d mm xa) => [pa pb]; apply: Zo_i => // t tr ts. move: (mm) => [m1 m2 m3]. case: (inc_or_not x t) => xt; last first. have ta: sub t (Ex4_11EM M x). move => s st; move: (ts _ st); case /setU1_P => // sx; case: xt; ue. by move: (m2 _ (sub_trans ta pa) tr). set x0 := Ex4_11EM M x. have qa: [/\ inc x0 (\Po A), sub x0 M & inc (x0 +s1 x) R]. rewrite /x0;split => //; apply /setP_P => //; apply: (sub_trans pa m1). set x1 := (t -s1 x). have ta: t = x1 +s1 x by symmetry;apply:setC1_K. have tb: sub (t -s1 x) M. move => s /setC1_P [sa sb]; move: (ts _ sa); case /setU1_P => //; apply: pa. have qb: [/\ inc x1 (\Po A), sub x1 M & inc (x1 +s1 x) R]. rewrite /x1;split => //; [by apply /setP_P; apply: (sub_trans tb m1) | ue ]. move /unique_existence: (Exercise4_11c mm xa) => [_ un]. by rewrite (un _ _ qa qb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)