proposition: Lemma Ex4_11_ex3a A R: (forall x, inc x R -> sub x A) -> (forall x, inc x A -> inc (singleton x) R) -> mobile_r R.
proof: Proof. move => RA h X Y xr yr xny z /setI2_P [zX zY]. case: (p_or_not_p (sub X Y)) => xsy. move: (rep_i (setC_ne (conj xsy xny))). set w := (rep (Y -s X)) => /setC_P [ra rb]. exists (singleton w);split => //. apply: h; apply: (RA _ yr _ ra). by move => t /set1_P ->; apply /setU2_P;right. move /set1_P; contradict rb; ue. have [w wx wny]: exists2 w, inc w X & ~ (inc w Y). ex_middle bad; case: xsy => t tx; ex_middle ty; case: bad; ex_tac. exists (singleton w);split => //. apply: h; apply: (RA _ xr _ wx). by move => t /set1_P ->; apply /setU2_P; left. by move /set1_P => zw; case: wny ; rewrite - zw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)