proposition: Lemma consec_pow_pr7 r r' f x: order_isomorphism f r r' -> inc x (substrate r) -> consec_pow r x = consec_pow r' (Vf f x).
proof: Proof. move => ha hb. rewrite/consec_pow. set T := consec_lists_for _ _. set T' := consec_lists_for _ _. congr union; set_extens k => /funI_P[t tT ->];apply /funI_P. move/consec_pow_pr0: tT => h. move: (consec_pow_pr6 ha h); set g := Lg _ _ => h'. by exists g; [ by apply /consec_pow_pr0 | rewrite /g; aw ]. move:(inverse_order_is ha) => hc. move/consec_pow_pr0: tT => h. move: (consec_pow_pr6 hc h); set g := Lg _ _. move: ha => [_ _ [bf sf _] _]. have xsf: inc x (source f) by ue. rewrite (inverse_V2 bf xsf) => h'a. by exists g; [ by apply /consec_pow_pr0 | rewrite /g; aw ]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)