proposition: Lemma Ex4_11_ex3b A n (R := Zo (\Po A) (fun z => nonempty z /\ cardinal z <=c n)): natp n -> n <> \0c -> mobile_r R.
proof: Proof. move => nb nz. have pa: (forall x, inc x R -> sub x A). by move => x =>/Zo_P [] /setP_P. apply: (Ex4_11_ex3a pa). move => x xA; apply: Zo_i; first by apply /setP_P;apply: set1_sub. split; fprops; rewrite cardinal_set1; apply: cge1;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)