proposition: Lemma IFE_consec_chain3 f x : inc x IFSE -> inc f (consec_lists_for IFS_order x) -> domain f <=c IFS_pow x.
proof: Proof. move => xE /consec_pow_pr0 [hf1 xrf]. move: (IFE_consec_chain1 hf1) =>[y yE fp]. move: hf1 =>[qa qb qc qd]. move/(range_gP qa):xrf =>[n ndf ->]; rewrite (fp _ ndf); aw. move /Zo_P:yE => [/setX_P [px /setX_P [ppx ppn qpn] qpq] gy]. case: (equal_or_not (domain f) \0c). by move ->; apply: cle0x; apply:CS_succ. move => dp. move: (cpred_pr qb dp); set s := cpred _; move =>[sa sb]. have sdf: inc s (domain f) by rewrite sb; apply: Nsucc_i. have fe: inc (Vg f s) IFSE. rewrite - (proj2 (IFE_osr)); apply: qc; apply/(range_gP qa); ex_tac. move/Zo_P:fe => [/setX_P [pxs /setX_P [pps ppns qpns] qpqs]]. rewrite /IFS_good_pair; rewrite (fp _ sdf); aw => eqa. move: (cleT (csum_Mle0 (Q (P y)) (CS_nat sa)) eqa). by rewrite /IFS_pow; aw; move/cleSS; rewrite sb. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)