proposition: Lemma IFE_consec_chain x : inc x IFSE -> consec_list_for IFS_order (IFS_chain x) x.
proof: Proof. move => xE. set m := csucc (Vf sigma (P (P x))). move/Zo_P: (xE) => [/setX_P [ra /setX_P [rb rc rd] re] rf]. have fgf: fgraph (IFS_chain x). by rewrite/IFS_chain; fprops. have df: (domain (IFS_chain x)) = m by rewrite /IFS_chain; aw. move/permutationsP: sp =>[bs ss ts]; move: (proj1 (proj1 bs)) => fs. have Sn1: natp (Vf sigma (P (P x))) by rewrite /natp; Wtac. have Sn: natp m by apply: NS_succ. split; last first. have hu: inc (Q (P x)) m by apply/NleP. apply/(range_gP fgf); rewrite df; exists (Q (P x)) => //. by rewrite/IFS_chain LgV// rb ra. have sr := (proj2 (IFE_osr)). have H i: i <c m -> inc (Vg (IFS_chain x) i) IFSE. move => lt1. move: (NS_lt_nat lt1 Sn) => iN. move/(NltP Sn): (lt1) => yb. rewrite /IFS_chain LgV//; apply/Zo_P; split. by apply: setXp_i => //; apply: setXp_i. by rewrite/IFS_good_pair; aw; apply/NleP. split. - done. - by rewrite /IFS_chain; aw. - move => t /(range_gP fgf) [y ya ->]; rewrite df in ya. by rewrite sr; move/(NltP Sn): (ya) => /H yb. move => i iN; rewrite df => lt1. move: (H _ lt1) => siE. have lt0 := (cle_ltT (cleS iN) lt1). move: (H _ lt0) => iE. have lt2: inc (csucc i) m by apply NltP. have lt3: inc i m by apply NltP. by apply/(IFE_consecP iE siE); rewrite /IFS_chain ! LgV//; aw. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)