proposition: Lemma card_dominant_pr10 a b (A := \aleph a) (B:= \aleph b) (X := A ^c B) (C := (the_nondominant_least A B)): ordinalp a -> ordinalp b -> \2c ^c B <c X -> ~ (rel_strong_card A B) -> [/\ rel_strong_card C B, singular_cardinal C, \cf C <=c B, B <c C & X = gimel_fct C].
proof: Proof. move => oa ob lt2 nsr. move: (CIS_aleph oa) (CIS_aleph ob) => ia ib. move: (the_nondominant_least_pr1 nsr (proj1 ia)). rewrite -/C; move => [pa pb pc]. move: (card_dominant_pr9 ib pa pb); rewrite -/A -/B -/C => eq1. have na2b: ~(A <=c \2c ^c B). move => bad. move: (cpow_Mleeq B bad (aleph_nz oa)). by rewrite - cpow_pow (csquare_inf ib) => /(cltNge lt2). have cc:=(proj31_1 pa). case: (cleT_el cc (proj1 ib)) => lBC. case: na2b. have cp := (CS_pow \2c B). case: (equal_or_not C \0c) => cnz. move: pb; rewrite cnz (cpow0x (aleph_nz ob)) => le2. exact: (cleT le2 (cle0x cp)). case: (equal_or_not C \1c) => cno. move: pb; rewrite cno cpow1x => le2. exact: (cleT le2 (cge1 cp (@cpow_nz _ B card2_nz))). by rewrite - (infinite_power1_a (cge2 cc cnz cno) lBC ib). have pd:rel_strong_card C B. move => t tC. case: (cleT_el cc (CS_pow t B)) => // cb. move: (card_dominant_pr9 ib tC cb); rewrite -/B => le1. rewrite le1 in pb. case: (cltNge tC (pc _ (cle_ltT (proj1 tC) pa) pb)). have ic: infinite_c C by apply: (cle_inf_inf ib (proj1 lBC)). move: (ord_index_pr1 ic); set c:= (ord_index C); move => [oc qb]. rewrite -qb in pd. move: (card_dominant_pr8 oc ob pd); rewrite qb -/B; move => [pe pf]. rewrite qb in pd. case: (cleT_el (CS_cofinality (proj1 cc)) (proj1 ib)) => h. move: (cle_ltT h lBC) => [_ ne]. by rewrite - (pf h) - eq1. by move: pb; rewrite (pe h) => /(cltNge pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)