proposition: Lemma IFS_sub_pow_prop1 x : inc x IFSE -> cardinal (IFS_sub_pow x) = csucc (P (P x)).
proof: Proof. move => xE; rewrite (IFS_sub_pow_prop0 xE). move/Zo_P:(xE) => [/setX_P [px /setX_P [ppx ppn qpn] qpq] gp]. rewrite cardinal_fun_image ?(card_card (CS_succ _)) //. move => a b /(NleP ppn) la /(NleP ppn) lb. move/permutationsP: sp => [ [[ff fi] _] ss ts]. have aN: inc a (source sigma) by rewrite ss; apply:(NS_le_nat la ppn). have bN: inc b (source sigma) by rewrite ss; apply:(NS_le_nat lb ppn). move: (Vf_target ff aN) (Vf_target ff bN); rewrite ts. by move=> /CS_nat ca /CS_nat cb; move/(csucc_inj ca cb); apply: fi. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)