proposition: Lemma card_dominant_pr8 a b (A := \aleph a) (B:= \aleph b) (X := A ^c B): ordinalp a -> ordinalp b -> rel_strong_card A B -> ( (B <c \cf A -> X = A) /\ (\cf A <=c B -> X = gimel_fct A)).
proof: Proof. move => oa ob sab. move: (CIS_aleph oa) (CIS_aleph ob) => ia ib. move: (infinite_power9 ia ib) => [_ _ i9]; exact (i9 sab). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)