proposition: Lemma infinite_power1_b x: infinite_c x -> x ^c x = \2c ^c x.
proof: Proof. move => ix; apply: infinite_power1_a => //. apply: cle_fin_inf => //; apply /NatP; fprops. exact (cleR (proj1 ix)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)