proposition: Lemma IFS_sub_pow_prop4 n a b (qa := IFS_sub_pow a) (qb := IFS_sub_pow b): natp n -> inc a IFSE -> inc b IFSE -> cardinal qa = csucc n -> cardinal qb = csucc (csucc n) -> union (qb -s qa) = csucc (Vf sigma (csucc n)).
proof: Proof. move => nN aE bE; move: (NS_succ nN) => sN. move/Zo_P:(aE) => [/setX_P [pa /setX_P [ppa ppna qpna] qpqa] gpa]. move/Zo_P:(bE) => [/setX_P [pb /setX_P [ppb ppnb qpnb] qpqb] gpb]. rewrite (IFS_sub_pow_prop1 aE) (IFS_sub_pow_prop1 bE). move/(csucc_inj (CS_nat ppna) (CS_nat nN)) => ra. move/(csucc_inj (CS_nat ppnb) (CS_succ n)) => rb. rewrite / qa / qb (IFS_sub_pow_prop0 aE) (IFS_sub_pow_prop0 bE). rewrite ra rb (succ_of_nat sN) funI_setU1; set U := fun_image _ _; set k := csucc _. suff: (U +s1 k -s U) = singleton k by move ->; rewrite setU_1. apply: set1_pr; last by move => t /setC_P [/setU1_P]; case => //. apply /setC_P; split; [ fprops | move/funI_P => [t /(NltP sN) ta tb]]. move/permutationsP: sp => [ [[ff fi] _] ss ts]. have aN: inc (csucc n) (source sigma) by rewrite ss. have bN: inc t (source sigma) by rewrite ss; apply:(NS_lt_nat ta sN). move: (Vf_target ff aN) (Vf_target ff bN); rewrite ts. move=> /CS_nat ca /CS_nat cb; move/(csucc_inj ca cb): tb. by move/(fi _ _ aN bN) => hh; case: (proj2 ta). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)