proposition: Lemma cpow_inf a n: infinite_c a -> natp n -> n <> \0c -> a ^c n = a.
proof: Proof. move => ai; move:n; apply: Nat_induction => // n nN hrec _. case: (equal_or_not n \0c) => nz. by rewrite nz succ_zero (cpowx1 (proj1 ai)). by rewrite (cpow_succ _ nN) (hrec nz) (csquare_inf ai). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)