proposition: Lemma infinite_power1_c x: infinite_c x -> (cnext x) ^c x = \2c ^c x.
proof: Proof. move=> ix; move:(ix) =>[cx _]. apply: infinite_power1 => //; last by apply: (cnext_pr3 cx). exact: (cleT (cle_fin_inf finite_2 ix) (proj1 ((cnext_pr2 cx)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)