proposition: Lemma cpow_inf1 a n: infinite_c a -> natp n -> (a ^c n) <=c a.
proof: Proof. move=> ia nN. case: (equal_or_not n \0c) => h. rewrite h cpowx0; apply: (cle_fin_inf finite_one ia). rewrite (cpow_inf ia nN h);apply:cleR; exact: (proj1 ia). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)