proposition: Lemma the_nondominant_least_pr2 a b (A := \aleph a) (B:= \aleph b) (c := (ord_index (the_nondominant_least A B))): ~ (rel_strong_card A B) -> ordinalp a -> ordinalp b -> (A <=c \2c ^c B) \/ [/\ c <o a, A <=c \aleph c ^c B & (forall t, t <o a -> A <=c \aleph t ^c B -> c <=o t)].
proof: Proof. move => h oa ob. move: (the_nondominant_least_pr1 h (CS_aleph oa)). set C := the_nondominant_least A B; move => [pa pb pc]. have cc:= proj31_1 pa. case: (finite_or_infinite cc) => ifc. left. have bnz: B <> \0c by apply: aleph_nz. have iB:= (CIS_aleph ob). have cp:= (CS_pow \2c B). case: (equal_or_not C \0c) => cnz. move: pb; rewrite cnz (cpow0x bnz) => 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))). have c2:= (cge2 cc cnz cno). have le1: C <=c B by apply: cle_fin_inf. have <- //: C ^c B = \2c ^c B by apply: infinite_power1_a. right. move: (ord_index_pr1 ifc); rewrite {1 2}/C -/c; move => [oc ac]. have ltca: c <o a by apply aleph_ltc_lt => //; rewrite ac. rewrite ac; split => //. move => t ta tb. have lt1: \aleph t <c A by apply: aleph_lt_ltc. move: (pc _ lt1 tb); rewrite -ac; apply: (aleph_lec_le oc (proj31_1 ta)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)