proposition: Lemma Exercise4_11d M x: max_pure A R M -> inc x (A -s M) -> (sub (Ex4_11EM M x) M /\ inc ((Ex4_11EM M x) +s1 x) R).
proof: Proof. move => pa pb; 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)). by rewrite - (select_uniq h qa (conj qb qc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)