proposition: Lemma reindex : pow_chain =p lift_chain [f ^^ pow_chain by cont_mono C].
proof: Proof. move=>x; split. - case; case=>[|n][->] /=; first by left. by right; exists (pow n); split=>//; exists n. case=>/=; first by move=>->; exists 0. by case=>y [->][n][->]; exists n.+1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)