proposition: Lemma Ex4_11_ex2_pure A (R := Zo (\Po A) (fun z => cardinal z = \2c)): (set_of_pure A R = Zo (\Po A) small_set /\ ( nonempty A -> forall M, max_pure A R M <-> (sub M A /\ singletonp M))).
proof: Proof. have pa:forall M, sub M A -> small_set M -> pure R M. move => M ma mb x xm => /Zo_P. move =>[_ cx2]; move: (sub_smaller xm); rewrite cx2. move /(cle2P); move => [a [b [am bm ab]]]. by case: ab;apply: (mb _ _ am bm). have pb: forall M, sub M A -> pure R M -> small_set M. move => M ma mb a b am bm; ex_middle ab. have sd: sub (doubleton a b) M by move => t; case /set2_P => ->. case: (mb _ sd); apply: Zo_i => //; last by apply: cardinal_set2. by apply /setP_P;apply:(sub_trans sd ma). split. set_extens t => /Zo_P [ta tb];apply: Zo_i => //; [ apply: pb | apply: pa] => //; apply /setP_P => //. move => neA M; split. move => [mc ma mb];move: (pb _ mc ma) => md; split; first by exact. case: (small_set_pr md) => // me. move: (rep_i neA) => rA. have qa: sub (singleton (rep A)) A by apply: set1_sub. have ps: pure R (singleton (rep A)). by apply: pa; [ move => t /set1_P => -> | apply: small1]. have sms: sub M (singleton (rep A)) by rewrite me; fprops. by rewrite (mb _ ps sms qa); exists (rep A). move => [ma [t st]]; split => //. by apply:pa => //; move => a b; rewrite st; move => /set1_P -> /set1_P ->. move: (set1_1 t); rewrite - st => tm. move => p pp mp pra; move: (pb _ pra pp) => py; apply: extensionality => //. by move => s sp; rewrite (py _ _ sp (mp _ tm)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)