proposition: Lemma infinite_power10_b x y: infinite_c x -> y <c (\cf x) -> y <> \0c -> x ^c y = x.
proof: Proof. move=> icx yc ynz. by move: (infinite_power10 y icx) => [_ pb _ _]; apply: pb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)