proposition: Lemma power_cofinality1 x: infinite_c x -> x <c x ^c (\cf x).
proof: Proof. move => icx; rewrite -(cofinality_card icx); apply: power_cofinality. by apply: infinite_ge2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)