proposition: Lemma sub_pow_pr0 r r' f x: order_isomorphism f r r' -> inc x (substrate r) -> IFS_sub_pow_gen r x = IFS_sub_pow_gen r' (Vf f x).
proof: Proof. move => fis xsr. rewrite /IFS_sub_pow_gen. set A := Zo _ _; set B := Zo _ _. move: (fis) => [or1 or2 [bf sf tf] fm]. have ff: function f by fct_tac. set_extens t. move=> /funI_P [z /Zo_P[zsr zle] ->]. rewrite (consec_pow_pr7 fis zsr). move: zsr xsr; rewrite - sf => zs xs. move/(fm z x zs xs): zle => fzle. apply/funI_P; exists (Vf f z) => //. apply:Zo_i => //; order_tac. move => /funI_P [z /Zo_P [za zb] ->]. rewrite - tf in za. move: (proj2 (proj2 bf) _ za) =>[y ya yb]. move: zb; rewrite yb => le1. rewrite sf in ya; rewrite - (consec_pow_pr7 fis ya). apply/funI_P; exists y => //; apply:(Zo_i ya). apply/fm => //; ue. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)