proposition: Lemma IFE_consec_chain1 f: consec_list IFS_order f -> exists2 x, inc x IFSE & forall i, inc i (domain f)-> Vg f i = J (J (P (P x)) (Q (P x) +c i)) (Q x).
proof: Proof. move => [qa qb qc qd]. case: (equal_or_not (domain f) \0c) => nz. move/permutationsP: sp =>[bs ss ts]; move: (proj1 (proj1 bs)) => fs. have iot: inc \1c (target sigma) by rewrite ts; apply: NS1. move: (inverse_V bs iot); set u := (Vf (inverse_fun _) _) => fu. exists (J (J u \0c) \0q); last by rewrite nz => t /in_set0. have qs0 := QS0; have ns0 := NS0. have uN: inc u Nat by rewrite - ss; exact: (inverse_Vis bs iot). apply/Zo_P; split. by apply: setXp_i => //; apply: setXp_i. rewrite /IFS_good_pair; aw; rewrite fu; apply: cle_01. have ze: inc \0c (domain f). by apply/(NltP qb); apply: card_ne0_pos => //; apply: CS_nat. have sr := (proj2 (IFE_osr)). set x := Vg f \0c. have xr: inc x (range f) by apply/(range_gP qa); ex_tac. have xsE: inc x IFSE by rewrite - sr; apply: qc. move /Zo_P: (xsE) => [/setX_P [px /setX_P [ppx ppn qpn] qpq] gpx]. ex_tac. move => i idf; move:(NS_inc_nat qb idf) => iN. move: i iN idf; apply: Nat_induction. by rewrite (csum0r (CS_nat qpn)) ppx px. move => n nN Hrec snd. have fsnE: inc (Vg f (csucc n)) IFSE. rewrite - sr; apply: qc; apply/(range_gP qa); ex_tac. move/(NltP qb): snd => lt1. move:(cle_ltT (cleS nN) lt1) => lt2. move/(NltP qb): lt2 => nd. have fnE: inc (Vg f n) IFSE. rewrite - sr; apply: qc; apply/(range_gP qa); ex_tac. move: (qd n nN lt1). move/(IFE_consecP fnE fsnE); rewrite (Hrec nd); aw; move => [ea eb ec]. move /Zo_P: (fsnE) => [/setX_P [pv /setX_P [ppv _ _] _] _]. by rewrite - pv - ppv - ec - ea - eb (csum_nS _ nN). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)