proposition: Lemma SCH_prop3 x y (z := x ^c y): infinite_c x -> \1c <=c y -> SingCardHypothesis -> ( (x <=c \2c ^c y -> z = \2c ^c y) /\ ((\2c ^c y <c x) -> ( (y <c \cf x -> z = x) /\ ((\cf x <=c y) -> z = cnext x)))).
proof: Proof. move => icx y1 sch; rewrite /z. have cy:= proj32 y1. have x2:= (infinite_ge2 icx). split => pa. apply: infinite_power1 => //. case: (finite_or_infinite cy) => // fy. have f2: finite_c (\2c ^c y). by apply /NatP; apply: NS_pow; fprops; apply /NatP. case: (finite_not_infinite (cle_fin_fin f2 pa) icx). have coi:=(cofinality_infinite_cardinal icx). case: (finite_or_infinite cy) => // fy. split => h. have yN: natp y by apply /NatP. rewrite (cpow_inf icx yN) //. by move/cge1P:y1 => [_ /nesym]. case: (cleNgt h (clt_fin_inf fy coi)). have yx:=(clt_leT (cantor (proj1 fy)) (proj1 pa)). move: (ord_index_pr1 icx); set c := (ord_index x); move => [oc cv]. pose p1 x y :=( y <c \cf x -> x ^c y = x) /\ (\cf x <=c y -> x ^c y = cnext x). pose p2 x := forall y, infinite_c y -> \2c ^c y <c x -> p1 x y. pose p c := p2 (\aleph c). rewrite -/(p1 _ _). suff: p2 x by move => h; apply: (h y). rewrite- cv. apply: (least_ordinal2 (p:= p)) oc => d od lyd. rewrite /p /p2. clear cy pa fy z y1 yx y. move => y icy yl1. have yx:=(clt_leT (cantor (proj1 icy)) (proj1 yl1)). case: (ordinal_limA od) => ln. by move: icy yx => / infinite_c_P2; rewrite ln aleph0E => h1 /(cleNgt h1). move: ln => [e oe es]. move: (CS_aleph oe) => ie. have l1: \2c ^c y <=c \omega e. by apply: cnext_pr4 => //; rewrite (cnextE oe) - es. have l2: (\aleph e) ^c y <=c \aleph d. case: (equal_or_not (\2c ^c y) (\aleph e)) => eq1. rewrite -eq1 - cpow_pow (csquare_inf icy);exact (proj1 yl1). have l3: \2c ^c y <c \omega e by split. have ed: e <o d by rewrite es; apply oltS. move: (lyd _ ed _ icy l3) => [q4 q5]. move: (CS_cofinality (proj1 ie)) => cc. case: (cleT_el cc (proj1 icy)) => cyx. rewrite (q5 cyx) (cnextE oe) -es; apply: cleR. by apply: CS_aleph. rewrite (q4 cyx); apply: aleph_le_lec;exact (proj1 ed). have l3: (\omega d) ^c y = \omega d. rewrite es (infinite_power2 oe (infinite_nz icy)). rewrite cprodC -es (cprod_inf l2 (CIS_aleph od)) //. by apply: cpow_nz ; apply: aleph_nz. move: (regular_initial_successor oe) => /regular_cardinalP [ _ h]. by rewrite /p1 es h -es; split => // /(cltNge yx). have aux: forall z, z <c (\omega d) -> z ^c y <c (\omega d). move => z z1. case: (finite_or_infinite (proj31_1 z1)) => fz. case: (equal_or_not z \0c) => znz. by rewrite znz (cpow0x (infinite_nz icy)) - znz. case: (equal_or_not z \1c) => zno. by rewrite zno cpow1x - zno. move: (cge2 (proj31_1 z1) znz zno) => z2. by rewrite (infinite_power1_a z2 (cle_fin_inf fz icy) icy). move: (ord_index_pr1 fz); set e := (ord_index z); move=> [z2 z3]. have ed: e <o d by apply: (aleph_ltc_lt z2 od); rewrite z3. case: (cleT_el (proj31_1 z1) (proj31_1 yl1)) => q1. by rewrite (infinite_power1 (infinite_ge2 fz) q1 icy). rewrite - z3 in q1. move: (lyd _ ed _ icy q1) => []; rewrite z3 => pa pb. move: (CS_cofinality (proj1 (proj1 fz))) => cc. case: (cleT_el cc (proj1 icy)) => cyx; last by rewrite (pa cyx). rewrite (pb cyx) - z3 (cnextE z2); apply: aleph_lt_ltc. move: ln => [_ _ ln1]; apply /oltP0. by split;fprops;apply: ln1; apply /oltP. move: (CIS_aleph od) => icz. move: (infinite_power9 icz icy) => [_ _ h]; move: (h aux) => [h1 h2]. split => p3; first by apply: h1. rewrite (h2 p3). exact (sch _ icz (cle_ltT (cpow_Meqle card2_nz p3) yl1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)