proposition: Lemma infinite_power2_bis x (y:= cnext x) m: infinite_c x -> m <> \0c -> y ^c m = (x ^c m) *c y.
proof: Proof. move=> ix mnz; rewrite /y;move: (ord_index_pr1 ix)=> [on <-]. rewrite (cnextE on); apply: (infinite_power2 on mnz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)