proposition: Lemma Exercise4_11d' M x M' : max_pure A R M -> inc x (A -s M) -> sub M' A -> sub M' M -> inc (M' +s1 x) R -> M' = Ex4_11EM M x.
proof: Proof. move => pa pb sm'a sm'm icm'xr; rewrite /Ex4_11EM. pose p z := sub z M /\ inc (z +s1 x) R; rewrite -/p -/(p _). move:(Exercise4_11c pa pb) => [z [[qa qb qc] zb]]. have h:(singl_val2 (inc ^~ (\Po A)) p). move => a b aP [r1 r2] bP [r3 r4]. by rewrite - (zb _ (And3 aP r1 r2)) (zb _ (And3 bP r3 r4)). apply: select_uniq => //. by apply/setP_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)