proposition: Lemma infinite_power6_5a a b : infinite_c b -> \aleph omega1 = a ^c b -> b = aleph0.
proof: Proof. move => /ord_index_pr1; set n := ord_index b;move => [on <-] eq. by move:(infinite_power6_5 OS1 on eq) => /olt1 ->; rewrite aleph0E. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)