proposition: Lemma Ex4_11_minR_pr3 A R (R' := min_incl_r R): mobile_ext R A -> (mobile_ext R' A /\ set_of_pure A R = set_of_pure A R').
proof: Proof. move => [pa pb pc pd]; move: (Ex4_11_minR_mb pb pc) => pe. split;last first. by set_extens t => /set_of_pureP [ta tb]; apply /set_of_pureP;split => //; move: tb; move /(Ex4_11_minR_P2 pb). have ta: ~ inc emptyset R' by move /Zo_P => [ta] _. split => // w => /Zo_S wr;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)