proposition: Lemma card_dominant_pr11 A B (X := A ^c B): infinite_c A -> infinite_c B -> [\/ X = A, X = \2c ^c B | exists C, [/\ infinite_c C, rel_strong_card C B, \cf C <=c B , B <c C & X = gimel_fct C]].
proof: Proof. move => ia ib. move: (ord_index_pr1 ia); set a:= (ord_index A); move => [oa qa]. move: (ord_index_pr1 ib); set b:= (ord_index B); move => [ob qb]. case: (equal_or_not (\2c ^c B) (A ^c B)) => eq0; first by constructor 2. have pa: \2c ^c B <c A ^c B. split => //; apply: (cpow_Mleeq B (infinite_ge2 ia) card2_nz). case: (cleT_el (proj1 ia) (proj1 ib)) => cab. constructor 2; exact :(infinite_power1_a (infinite_ge2 ia) cab ib). case: (p_or_not_p (rel_strong_card A B)) => sr. move: (card_dominant_pr8 oa ob); rewrite qa qb => h. move: (h sr) => [h1 h2]. have cco:=(CS_cofinality (proj1 (proj1 ia))). case: (cleT_el cco (proj1 ib)) => h3. constructor 3; exists A;split;fprops. by constructor 1 ; apply: h1. move: (card_dominant_pr10 oa ob). set C := the_nondominant_least _ _; rewrite qa qb. move => xx; move: (xx pa sr); move => [q1 q2 q4 q5 q6]. constructor 3; exists C; split => //. apply (cle_inf_inf ib (proj1 q5)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)