proposition: Lemma IFS_sub_pow_prop3 x (y := (IFS_sub_pow x)): inc x IFSE -> cardinal y = \1c -> union y = csucc (Vf sigma \0c).
proof: Proof. move => xE. move/Zo_P:(xE) => [/setX_P [px /setX_P [ppx ppn qpn] qpq] gp]. rewrite (IFS_sub_pow_prop1 xE) - succ_zero. move/(csucc_inj (CS_nat ppn) CS0) => pp. by rewrite /y (IFS_sub_pow_prop0 xE) pp succ_zero funI_set1 setU_1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)