proposition: Lemma IFS_sub_pow_prop2 n : natp n -> exists2 x, inc x IFSE & cardinal (IFS_sub_pow x) = csucc n.
proof: Proof. move => nN. set z := J (J n \0c) \0q. 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. by move/permutationsP: sp => [ [[ff _] _] ss ts]; rewrite /natp; Wtac; ue. by ex_tac; rewrite (IFS_sub_pow_prop1 zE) /z; aw. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)