proposition: Lemma Exercise4_11f M x y: max_pure A R M -> inc x (A -s M) -> inc y (Ex4_11EM M x) -> max_pure A R ((M +s1 x) -s1 y).
proof: Proof. move => mxpm xam ye; move: (Exercise4_11d mxpm xam) => [pa pb]. move: (mxpm) (xam) => [ma pm mpm] /setC_P [xa xm]. set T := ((M +s1 x) -s1 y). have tpP: forall u, inc u T <-> ((inc u M \/ u = x) /\ u <> y). move => u; split. by move /setC1_P =>[sa sb]; split => //; apply /setU1_P. by move => [sa sb]; apply /setC1_P;split => //; apply /setU1_P. have tA: sub T A. move => t /tpP []; case; [fprops | by move => ->]. move: mnr => [q1 q2 q3 q4]. split; first by exact. move => z zt zr. case: (inc_or_not x z) => xz; last first. apply: pm zr; move => t tz; move: (zt _ tz) => /tpP. move => [h _]; case: h => // tx; case: xz; ue. have xe: inc x ((Ex4_11EM M x) +s1 x) by fprops. have xnez: (Ex4_11EM M x) +s1 x <> z. move => ta. have : inc y ((Ex4_11EM M x) +s1 x) by fprops. by rewrite ta =>yz; move: (zt _ yz) => /tpP [_]. have xi: inc x ((Ex4_11EM M x) +s1 x \cap z) by fprops. move: (q3 _ _ pb zr xnez _ xi); move => [Z [ZR Zt xZ]]. have ZM: sub Z M. move => t tZ;move: (Zt _ tZ); case /setU2_P. case /setU1_P; [ by apply: pa | by move => tx; case: xZ; ue]. move => tz; move: (zt _ tz) => /tpP [ta tb]. case: ta => //;move => tx; case: xZ; ue. by case: (pm _ ZM). move => p pp sp pA. case: (inc_or_not y p) => yp. have st: sub (M +s1 x) A by move => t; case /setU1_P; fprops; move => ->. have pt: (pure R (M +s1 x)). move => s sst; apply: pp. move => t ts; case: (equal_or_not t y) => Tp; first by rewrite Tp. by apply: sp; apply /tpP;split => //; apply /setU1_P; apply: sst. have st1: sub M (M +s1 x) by fprops. case: xm; rewrite (mpm _ pt st1); fprops. ex_middle ntp. move: (setC_ne (conj sp ntp)) =>[v] /setC_P [vp vT]. have ynv: y <> v by move => yv;case: yp; rewrite yv. move: (pA _ vp) => vA. have pt: pure R (T +s1 v). have sa: sub (T +s1 v) p by move => t; case /setU1_P;[ apply:sp | move => ->]. move => b ba; apply: pp; apply: (sub_trans ba sa). have nvM: inc v (A -s M). apply /setC_P; split => //; move => vm. by case: vT; apply/tpP;split => //; [ left | apply:nesym ]. have xnv: x <> v by move => xv;case: vT; apply /tpP;split; fprops. move: (Exercise4_11d mxpm nvM); move => [sE iteR]. set Sx := ((Ex4_11EM M x) +s1 x). set Sv := ((Ex4_11EM M v) +s1 v). have s1: sub Sv A by move => t; case /setU1_P; fprops; move => ->. have s2: sub Sx A by move => t ; case /setU1_P ; fprops; move => ->. case: (inc_or_not y Sv) => yEv; last first. have BM: sub Sv (T +s1 v). move => t; case /setU1_P => te; apply/setU1_P; fprops; left. apply /tpP; split; first by left; apply: sE. dneg ty; apply /setU1_P; left; ue. by move: (pt _ BM). have yEx: inc y Sx by rewrite /Sx;fprops. have nSxv: Sx <> Sv. dneg sxv; have: inc x Sx by rewrite /Sx; fprops. by rewrite sxv /Sv;aw; case /setU1_P => // xv; case: xm; apply: sE. have yi: inc y (Sx \cap Sv) by fprops. move: (q3 _ _ pb iteR nSxv _ yi) => [Z [Zr zi nyz]]. have zt: sub Z (T +s1 v). move => t tz. have tny : t <> y by move => ty; case: nyz; ue. move: (zi _ tz); case /setU2_P; case /setU1_P => ta; apply /setU1_P. by left; apply /tpP;split => //; left; apply: pa. by left; apply /tpP;split => //; right. by left; apply /tpP;split => //; left; apply:sE. by right. by move: (pt _ zt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)