proposition: Lemma infinite_power10_a x: infinite_c x -> x ^c (\cf x) = cnext x.
proof: Proof. move => icx; move: (infinite_power10 (\cf x) icx) => [_ _ pa _]. have h:=(cofinality_small icx). apply: pa => //;apply (cleR (proj31 h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)