proposition: Lemma genconthypothesis_alt b: ordinalp b -> (forall a, ordinalp a -> \2c ^c (\aleph a) = \aleph (a +o b)) -> b <o omega0.
proof: Proof. move => ob h. have oo:= OS_omega. case: (oleT_el oo ob) => // lob. pose p x := b <o x +o b. have pb: p b. have pa: \0o <o omega0 by apply ordinal_finite3; fprops;apply emptyset_finite. move: (osum_Meqlt (olt_leT pa lob) ob); rewrite osum0r //. move: (least_ordinal4 ob pb); set a := least_ordinal p b. move => [oa pa al]. have ab: a <=o b by apply: al. have a0: \0o <o a. move: pa; rewrite /p - {1} (osum0l ob); apply: (osum_Mlteqr OS0 oa ob). have paa : a <o a +o a by move: (osum_Meqlt a0 oa); rewrite osum0r. case: (ordinal_limA oa) => nz; first by case: (proj2 a0). move: nz => [m om mv]. have pm: p m. move: OS1 pa; rewrite /p mv => o1. rewrite - osucc_pr // - osumA // osum_1inf //. by move: (al _ om pm); rewrite mv; move/(oltNge (oltS om)). set k := \aleph (a +o a). have oaa:=(OS_sum2 oa oa). have sk: singular_cardinal k. split; first by apply:CIS_aleph. have laa:= (osum_limit oa nz). have anz: a <> \0o by apply: limit_nz. rewrite /k (regular_initial_limit1 laa) (cofinality_sum oa a0). move=> bad; move: (cofinality_pr3 oa); rewrite bad. move: (aleph_pr6 oaa) => le1 le2. case: (oltNge paa (oleT le1 le2)). set s1 := \aleph (a +o b). have pc : forall c, c<o a -> \2c ^c (\aleph (a +o c)) = s1. move => c ca. have oc:= proj31_1 ca. have oac: ordinalp (a +o c) by apply: OS_sum2 => //. rewrite (h _ oac) - (osumA oa oc ob). have <- //: b = (c +o b). ex_middle neq. have p1: b <=o c +o b by apply osum_M0le. case: (oltNge ca (al _ oc (conj p1 neq))). have pd: forall c, a<=o c -> c<o a +o a -> \2c ^c (\aleph c) = s1. move=> c ac caa; move: (odiff_pr ac) => [qa qb]. rewrite qb in caa; move: (osum_Meqltr qa oa oa caa) => da. by move: (pc _ da); rewrite -qb. have px: (cpow_less_ecb k). exists (\aleph a); first by apply: (aleph_lt_ltc paa). move=> c c1 c2. move: (cle_inf_inf (CIS_aleph oa) c1) => ic. move: (ord_index_pr1 ic) => [om mv]. rewrite (pd _ (oleR oa) paa). rewrite -mv in c1 c2. have p1:= (aleph_lec_le oa om c1). have p2:= (aleph_ltc_lt om oaa c2). by rewrite -mv (pd _ p1 p2). move: (cpow_less_pr10 sk px); rewrite (h _ oaa). set s2 := \aleph ((a +o a) +o b) => eq1. have c12: s1 <c s2. apply: aleph_lt_ltc; rewrite - osumA //; apply: osum_Meqlt => //. suff: \2c ^<c k <=c s1 by rewrite - eq1 => /(cltNge c12). apply:card_ub_sup; first exact: (proj31_1 c12). move => i /funI_P [z zv ->]. have ck: cardinalp k by move: sk => [[ok _] _]. move: zv => /(cardinals_ltP ck) zv. have cz:=proj31_1 zv. have is1: infinite_c s1 by apply: CIS_aleph; apply: OS_sum2. case: (finite_or_infinite cz) => fz. apply: cle_fin_inf => //. by apply /NatP; apply: NS_pow; fprops; apply /NatP. move: (ord_index_pr1 fz)=> [om zv1]. have lt1: (ord_index z) <o a +o a. by apply: (aleph_ltc_lt om oaa); rewrite zv1 -/k. rewrite - zv1. case: (oleT_ee oa om) => le1. by rewrite (pd _ le1 lt1); apply: cleR; move: is1 => []. by rewrite (h _ om); apply: aleph_le_lec; apply: osum_Mleeq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)