proposition: Lemma consec_pow_pr6 r r' f g x (g' := Lg (domain g) (fun z => Vf f (Vg g z))): order_isomorphism f r r' -> consec_list_for r g x -> consec_list_for r' g' (Vf f x).
proof: Proof. move => iso [qa qb]. move:(order_isomorphism_sincr iso) => fsi. move: iso => [or or' [fp sf tf] fm]. have ra: fgraph g' by rewrite /g'; fprops. have rb: domain g' = domain g by rewrite /g'; aw. move: qa => [sa sb sc sd]. split; last first. move/(range_gP sa): qb =>[y ya ->]. apply/(range_gP ra); rewrite rb; ex_tac; rewrite /g' LgV//. have ff: function f by fct_tac. have sc1 i: inc i (domain g) -> inc (Vg g i) (substrate r). move => h; apply: sc;apply/(range_gP sa); ex_tac. split; [ done | ue | | ]. move => t/(range_gP ra); rewrite rb; move => [yy ya ->]. by rewrite /g' LgV//; Wtac; rewrite sf; apply: sc1. rewrite rb. move => i iN lt; rewrite /g'. have qa: inc (csucc i) (domain g) by apply /NltP. have qc: inc i (domain g). apply /(NltP sb); exact: (cle_ltT (cleS iN) lt). move: (sd i iN lt) =>[rc rd]. rewrite !LgV//;split; first by apply: fsi. move => z zs [z1 z2]. have ztf: inc z (target f) by ue. move: (proj2 (proj2 fp) z ztf) => [t ta tb]. move: z1 z2; rewrite tb ;move =>[z1 z2][z3 z4]. have x2s: inc (Vg g (csucc i)) (source f) by rewrite sf; apply: sc1. have x1s: inc (Vg g i) (source f) by rewrite sf; apply: sc1; apply: qc. have tsr: inc t (substrate r) by ue. case (rd t tsr); split; split. - by move/(fm (Vg g i) t x1s ta): z1. - by move => h; case: z2; rewrite h. - by move/(fm t (Vg g (csucc i)) ta x2s): z3. - by move => h; case: z4; rewrite h. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)