proposition: Lemma IFS_sub_pow_prop0 x : inc x IFSE -> IFS_sub_pow x = fun_image (csucc (P (P x))) (fun z => csucc (Vf sigma z)).
proof: Proof. move => xE. move/Zo_P:(xE) => [/setX_P [px /setX_P [ppx ppn qpn] qpq] gp]. set_extens t. move/funI_P => [z /Zo_P[zE lzx] -> ]. rewrite (IFE_consec_chain4 zE); apply/funI_P. have h: P (P x) <=c P (P x) by apply: (cleR (CS_nat ppn)). have la: P (P z) <=c P (P x). move/IFE_gleP: lzx => /proj33;case. - by case. - by move => [ -> _]. - by move => [ -> _ _]. by exists (P (P z)) => //; apply/(NleP ppn). move/funI_P =>[m /(NleP ppn) mle -> ]; apply/funI_P. case /cle_eqVlt: mle => mle. rewrite mle; exists x. move: IFE_osr =>[or sr]. by apply:Zo_i => //; order_tac; rewrite sr. by rewrite (IFE_consec_chain4 xE). set z := J (J m \0c) \0q. have mN: natp m by apply: (NS_lt_nat mle ppn). have zE: inc z IFSE. apply: Zo_i. by move: NS0 QS0 => ra rb; apply: setXp_i => //; apply:setXp_i. rewrite /IFS_good_pair /z; aw; apply: cle0n. move/permutationsP: sp => [ [[ff _] _] ss ts]; rewrite /natp; Wtac; ue. have zz: glt IFS_order z x. by apply/IFE_gltP; split => //;constructor 1; rewrite /z; aw. exists z. apply: (Zo_i zE); exact: (proj1 zz). by rewrite (IFE_consec_chain4 zE); rewrite /IFS_pow/z; aw. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)