proposition: Lemma card_dominant_pr4 (b:= least_non_trivial_dominant): [/\ card_dominant b, omega0 <c b, (forall z, card_dominant z -> omega0 <c z -> b <=c z), (b ^c omega0 = omega0 ^c b) & (b ^c omega0 = \2c ^c b) /\ (b ^c omega0 = (\2c ^c b) ^c b) ].
proof: Proof. have co:= CS_omega. move: (next_dominant_pr co) (card_dominant_pr3 co). rewrite (_: (next_dominant omega0) = b ) //. move => [pa pb pc] pd; move: (pa) => [pf _]. have io: infinite_c omega0 by rewrite - aleph0E; apply: CIS_aleph; fprops. have pe: omega0 ^c b = \2c ^c b. apply: infinite_power1_a => //. apply: cle_fin_inf;fprops. apply: (proj1 pb). by rewrite - cpow_pow (csquare_inf pf) pe pd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)