proposition: Lemma Exercise6_22c2 x (p1 := forall z, \0c <c z -> z <c x -> x ^c z = x) (p2:= forall z, \0c <c z -> x ^c z = x *c \2c ^c z): [/\ (infinite_c x -> p1 -> p2), (card_dominant x -> (p1 <-> p2)), (card_dominant x -> p1 -> (x = omega0 \/ inaccessible x)) & (x = omega0 \/ inaccessible x -> (card_dominant x /\ p1))].
proof: Proof. have r1:infinite_c x -> p1 -> p2. move=> icx hp1 z zp. move: (infinite_ge2 icx) => x2. move: (infinite_nz icx) => xnz. have cz:= proj32_1 zp. case: (cleT_ee (proj1 icx) (CS_pow \2c z)). move => le1. move: (cle_inf_inf icx le1) => icp. case: (finite_or_infinite cz) => icz. have f1: finite_c (\2c ^c z). by apply /NatP; apply NS_pow; fprops; rewrite inc_Nat. case: (finite_not_infinite f1 icp). rewrite (infinite_power1 x2 le1 icz). by rewrite cprodC cprod_inf. have pnz: \2c ^c z <> \0c by apply: cpow2_nz. move => le1. rewrite (hp1 _ zp (clt_leT (cantor cz) le1)). rewrite cprod_inf //. have r2: card_dominant x -> (p1 <-> p2). move=> [icx cdx]; split; first by apply: r1. move => hp2 z z0 zx. have pnz: \2c ^c z <> \0c by apply: cpow2_nz. move: (cdx _ _ (clt_fin_inf finite_2 icx) zx) => [l1 _]. rewrite (hp2 _ z0) cprod_inf //. have r3: card_dominant x -> p1 -> x = omega0 \/ inaccessible x. move => pa pc; case: (Exercise6_22c1 pa); first by left. move => h; right. move: pa => [pa pb]. split; last first. by move => t tx; apply: pb => //; apply: (clt_fin_inf finite_2 pa). split; last by exact. move: (cofinality_c_small (proj1 pa)) => h1. split => //; ex_middle eq1. have pd: \0c <c cofinality_c x. apply: (clt_fin_inf finite_0 (cofinality_infinite pa)). move: (power_cofinality (infinite_ge2 pa)). by rewrite (pc _ pd (conj h1 eq1)); move => [_]. split => //. case => ix. rewrite ix; split; first by apply: card_dominant_pr2. move => z z0 zf. have pa: infinite_c x by rewrite ix; apply: CIS_omega. have pb: inc z Nat. by rewrite ix in zf; move: (oclt zf) => /oltP0 [_ _]. have pc: z <> \0c by move: z0 => [_ /nesym]. by rewrite cpow_inf. split; first by apply: inaccessible_dominant. by move => z [_ zc] zx;apply: inaccessible_pr7 => //; apply:nesym. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)