proposition: Lemma opow_int_omega n: \2o <=o n -> n <o omega0 -> n ^o omega0 = omega0.
proof: Proof. move=> n2 no. have oo:= OS_omega. have on:= proj32 n2. have nz:=(olt_leT olt_02 n2). apply:oleA. rewrite (proj2 (opow_normal n2) _ omega_limit). apply: ord_ub_sup => //. by move => x /funI_P [z /(oltP oo) /(opow_2int1 no) [zo _] ->]. by move: (opow_Mspec2 oo n2); rewrite oprod_int_omega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)