proposition: Lemma exercise_6_19b a (ba := ord_index (cofinality (\aleph a))) (x := \aleph a) (y := \aleph ba): ordinalp a -> (x <c x ^c y /\ (forall n c, cardinalp n -> ordinalp c -> x = n ^c (\aleph c) -> c <o ba)).
proof: Proof. move => oa. move: (CIS_aleph oa) => io. move: (cofinality_pr3 (proj1 (proj1 io))). move: (cofinality_infinite io). rewrite (cofinality_card io) =>pa pd. move: (cofinality_card io) => H. move: (ord_index_pr1 pa) => [pb]; rewrite - /ba -/y -/x - H. move => yc. split. rewrite yc; apply: power_cofinality. by apply: infinite_ge2; apply: CIS_aleph. move => n c cn oc eq. have qa: \2c <=c n. apply: cge2 => //. move=> n0; move: eq; rewrite n0 cpow0x; by apply: aleph_nz. move => n1; move: eq; rewrite n1 cpow1x => x1. move: (CIS_aleph oa); rewrite -/x x1. apply: finite_not_infinite; fprops. have qb:infinite_c (\aleph c) by apply: CIS_aleph. move: (power_cofinality5 qa qb); rewrite -eq - H - yc => l2. apply: aleph_ltc_lt => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)