proposition: Lemma Ex4_11_ex1_pure A n (R := Zo (\Po A) (fun z => finite_set z /\ n <c cardinal z)): inc n Nat -> [/\ set_of_pure A R = Zo (\Po A) (fun z => cardinal z <=c n), (n <=c cardinal A -> forall M, sub M A -> (max_pure A R M <-> cardinal M = n)) & (cardinal A <=c n -> (set_of_pure A R = \Po A /\ (forall M, max_pure A R M <-> M = A)))].
proof: Proof. move => nN. have pa: forall P, sub P A -> pure R P -> cardinal P <=c n. move => p pa pb. case: (cleT_el (CS_cardinal p) (CS_nat nN)) => // h. case: (finite_or_infinite (CS_cardinal p)) => fcp. by case: (pb _ (@sub_refl p)); apply: Zo_i => //;apply /setP_P. have fsc: finite_c (csucc n) by apply /NatP; fprops. move: (card_card (CS_succ n)) => csn. move: (cle_fin_inf fsc fcp). rewrite - csn; move => /eq_subset_cardP1/set_leP [z zp]. move /card_eqP; rewrite csn => zc. case: (pb _ zp);apply: Zo_i. apply /setP_P; apply: (sub_trans zp pa). split; first by rewrite /finite_set - zc; apply /NatP; fprops. rewrite - zc; fprops. have pb: forall P, (sub P A /\ cardinal P <=c n) -> pure R P. move => p [qa qb]. move => x xp xr; move: (sub_smaller xp) => le1. move: (cleT le1 qb) => le2. by move: xr => /Zo_P [_ [_ /(cleNgt le2)]]. split. set_extens t; move /Zo_P => [ta tb]; apply /Zo_P;split => //. by apply: pa => //; apply /setP_P. by apply: pb;split => //;apply /setP_P. move => ca M mc; split. move => [_ ma mb]; ex_middle ce1; move: (pa _ mc ma) => le1. have cm: cardinal M <c n by split. have ss: ssub M A. by split => // bad; rewrite -bad in ca; case: ce1; apply:cleA. move: (rep_i (setC_ne ss)); set w := rep _. move => /setC_P [sa sb]; move: (csucc_pr sb); set p := M +s1 w => cp. have sp: sub p A. by move => t; case/setU1_P; [apply: mc | by move => -> ]. have pp: pure R p. apply: pb; split => //; rewrite cp; apply /cleSlt0P; fprops. have mp: sub M p by move => t tm ; apply /setU1_P; fprops. case: sb; rewrite (mb _ pp mp) //; rewrite /p; fprops. move => cm; split => //; first by apply: pb; split => //; rewrite cm; fprops. move => p pp mp spa; move: (pa _ spa pp) => px. have fsm: finite_set p by apply /NatP; apply:(NS_le_nat px nN). by apply: (strict_sub_smaller_contra fsm mp); apply: cleA; [apply:sub_smaller | ue]. move => le1. have pd: (forall M, sub M A -> pure R M). move => m ma; apply: pb; split => //; exact: (cleT (sub_smaller ma) le1). split. set_extens t; first by move /Zo_P => []. by move /setP_P => ta; apply /set_of_pureP;split => //; apply: pd. have pra: pure R A by apply: pd. move => M; split; first by move => [ma sa mb]; apply: mb => //. move => ->; split => //; move => p _; apply: extensionality. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)