proposition: Lemma fset_iterFE i : iterF i = [fsetval x in iter i Fsub set0].
proof: Proof. elim: i => [|i /= -> /=]; last by rewrite fset_fsub // F_bound//= fset_sub_val. by apply/fsetP=> x; rewrite in_fset_val /=; case: insub=> //= ?; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)