proposition: Lemma cnext_pow C x y: infinite_c C -> inc x (cnext C) -> inc y (cnext C) -> inc (x ^o y) (cnext C).
proof: Proof. move => ha hx; move: (ha) => [cc _]. move /(cnextP cc): (hx) => [ox cx] /(cnextP cc) [oy cy]. have s1: inc \1o (cnext C). by apply:cnext_leomega => //; move: olt_1omega => []. case: (ord2_trichotomy ox). case: (equal_or_not y \0o); first by move => ->; rewrite opowx0. move => ynz ->; rewrite opow0x //. apply:(cnext_leomega ha (proj1 olt_0omega)). by move => ->; rewrite opow1x. move => x2;move: y oy cy; apply:least_ordinal2 => z oz hz coz. have aux: forall t, t<o z -> inc (x ^o t) (cnext C). move => t sa; apply: (hz _ sa). exact: (cleT (ocle1 (proj1 sa)) coz). case: (ordinal_limA oz); first by move => ->; rewrite opowx0. move=> [t ot zt]. have tz: t <o z by rewrite (oltP oz) zt /osucc; fprops. move: (aux _ tz) => ee. by rewrite zt (opow_succ ox ot); apply: cnext_prod. move => lz. rewrite (proj2 (opow_normal x2) _ lz); apply: cnext_sup => //. apply: cleT coz; apply: fun_image_smaller. by move => j /funI_P [k /(oltP oz) kz ->];apply: aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)